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