Principia mathematica, by Alfred North Whitehead ... and Bertrand Russell.

SECTION B] DEDEKINDIAN RELATIONS 685
*214A42. F P e Ser n Ded P2=P. cx e sect'P. ). limaxp'c =limninp(C'P -a)
This proposition is important in dealing with Dedekind "cuts."
*214A43. F:.PeSerADed.cxesect'P. ):
limaxp'ca = liminp'(U'P - a)). V. maxp'a P1 minp'(G'P - a)
*214-5 shows that a Dedekindian relation has a beginning and an end;
the following propositions deal with P Ai J when P is Dedekindian.
*214-6 shows that a relation which is similar to a Dedekindian relation is
Dedekindian.
We call a relation "semi-Dedekindian" if it becomes Dedekindian by
the addition of one term at the end; the definition is
*21402. semiiDed FP(sect'P- t'O'P C 'maxp v tl'seqp) Df
*214-01. Ded= P ((a). a e '1maxP v Pseqp} Df
*214-02. semi Ded = P (sect'P- tIC'P C (I'maxp v U'seqp) Df
*21441. F P E Ded.. (a). ae tIrmaxp v EI'seqp [(*214-01)]
*2144101. F P EDed.. - Pmaxp C UI'seqp.. - U'maxp C U'ltp
[*214-1.- *24312. *207-12]
*214411. F: Pe Ded. =.((a)..a eU'Fmaxp u 'l1tpp.(a). aed('limaxp
[*214-1. *207-14-44]
*214412. F:. P e Ded. =C: a C'P.6 a e Cvmaxp v 1seqp
[*214-1. *205-151. *206131]
*214413. F:. P e trans. ): P E Ded.. sect'P C P11maxp v (l'seqp
[*211-272. *214-1]
*214-131. F:. F Ptrans.):P e Ded.-.D('PE A I) C EIseqp [*211-47.*214-1]
*2144132. F:. FE trans.:): FE Ded. E. D'Pe C t1"maxp v (Pseqp
[*214-131. *211-42]
*21414. F:.PeSer.3:PeDed. =.PeDed [*206-57.*214-l]
*2144141. F:. P FE Ser.: P E Ded. * (a) -p'P"(ca n C' P) e U'1maxp v U'seqp
[*206-56. *214-1]
*214-15. F:. Pe Ser. ): Pe Ded. D.D'Pe C 'seqp
[*206-36. *214-1. *211-11]
*2144151. F:.PeSer.: PeDed.-.DFPe=Pl"CP [*21138. *214-1]