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 that
A5: a in field R and
A6: 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 Th1;
hence b in Z by A6; :: 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 A7: ( a in field R & not a in Z ) ; :: according to TARSKI:def 3 :: thesis: contradiction
(field R) \ Z <> {} by A7, XBOOLE_0:def 5;
then consider a being set such that
A8: a in (field R) \ Z and
A9: for b being set st b in (field R) \ Z holds
[a,b] in R by A1, Th10;
not a in Z by A8, XBOOLE_0:def 5;
then consider b being set such that
A10: [b,a] in R and
A11: b <> a and
A12: not b in Z by A4, A8;
b in field R by A10, RELAT_1:15;
then b in (field R) \ Z by A12, XBOOLE_0:def 5;
then [a,b] in R by A9;
hence contradiction by A2, A10, A11, Lm3; :: thesis: verum