let R be Relation; :: thesis: ( R is well-ordering implies for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) ) )
assume A1: R is well-ordering ; :: thesis: for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
then A2: R is connected by Def4;
A3: R is antisymmetric by A1, Def4;
let a be set ; :: thesis: ( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
assume A4: a in field R ; :: thesis: ( for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
defpred S₁[ set ] means not [$1,a] in R;
given b being set such that A5: ( b in field R & not [b,a] in R ) ; :: thesis: ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) )
consider Z being set such that
A6: for c being set holds
( c in Z iff ( c in field R & S₁[c] ) ) from XBOOLE_0:sch 1();
for b being set st b in Z holds
b in field R by A6;
then A7: Z c= field R by TARSKI:def 3;
Z <> {} by A5, A6;
then consider d being set such that
A8: d in Z and
A9: for c being set st c in Z holds
[d,c] in R by A1, A7, Th10;
take d ; :: thesis: ( d in field R & [a,d] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R ) )
thus A10: d in field R by A6, A8; :: thesis: ( [a,d] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R ) )
A11: not [d,a] in R by A6, A8;
then a <> d by A8, A9;
hence [a,d] in R by A2, A4, A10, A11, Lm4; :: thesis: for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R
let c be set ; :: thesis: ( c in field R & [a,c] in R & not c = a implies [d,c] in R )
assume that
A12: c in field R and
A13: [a,c] in R ; :: thesis: ( c = a or [d,c] in R )
assume c <> a ; :: thesis: [d,c] in R
then not [c,a] in R by A3, A13, Lm3;
then c in Z by A6, A12;
hence [d,c] in R by A9; :: thesis: verum