let R be Relation; :: thesis: ( R is well-ordering & field R <> {} 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 & field R <> {} ) ; :: 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 & R is antisymmetric & R is reflexive & ( for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) ) ) by Def4, Th10;
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 A3: 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 ) ) )
given b being set such that A4: ( 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 ) )
defpred S₁[ set ] means not [$1,a] in R;
consider Z being set such that
A5: 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 A5;
then A6: Z c= field R by TARSKI:def 3;
Z <> {} by A4, A5;
then consider d being set such that
A7: ( d in Z & ( for c being set st c in Z holds
[d,c] in R ) ) by A1, A6, 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 A8: d in field R by A5, A7; :: 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 ) )
A9: not [d,a] in R by A5, A7;
then a <> d by A7;
hence [a,d] in R by A2, A3, A8, A9, 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 A10: ( c in field R & [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 A2, A10, Lm3;
then c in Z by A5, A10;
hence [d,c] in R by A7; :: thesis: verum