let R be Relation; :: thesis: ( R is well-ordering implies for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z )
assume A1: R is well-ordering ; :: thesis: for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z
then A2: R is antisymmetric by Def4;
let Z be set ; :: thesis: ( ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) implies field R c= Z )
assume A3: for a being set st a in field R & R -Seg a c= Z holds
a in Z ; :: thesis: field R c= Z

A4: now

let a be set ; :: thesis: ( a in field R & ( for b being set st [b,a] in R & a <> b holds
b in Z ) implies a in Z )
assume A5: ( a in field R & ( for b being set st [b,a] in R & a <> b holds
b in Z ) ) ; :: thesis: a in Z

now

let b be set ; :: thesis: ( b in R -Seg a implies b in Z )
assume b in R -Seg a ; :: thesis: b in Z
then ( [b,a] in R & b <> a ) by Def1;
hence b in Z by A5; :: thesis: verum

end;

then R -Seg a c= Z by TARSKI:def 3;
hence a in Z by A3, A5; :: thesis: verum

end;

given a being set such that A6: ( a in field R & not a in Z ) ; :: according to TARSKI:def 3 :: thesis: contradiction
(field R) \ Z <> {} by A6, XBOOLE_0:def 5;
then consider a being set such that
A7: ( a in (field R) \ Z & ( for b being set st b in (field R) \ Z holds
[a,b] in R ) ) by A1, Th10;
( a in field R & not a in Z ) by A7, XBOOLE_0:def 5;
then consider b being set such that
A8: ( [b,a] in R & b <> a & not b in Z ) by A4;
b in field R by A8, RELAT_1:30;
then b in (field R) \ Z by A8, XBOOLE_0:def 5;
then [a,b] in R by A7;
hence contradiction by A2, A8, Lm3; :: thesis: verum