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_{1}[ 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_{1}[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

( 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

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

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