let R be Relation; :: thesis: ( R is well-ordering implies for Z being set st ( for a being object 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 object st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z
let Z be set ; :: thesis: ( ( for a being object st a in field R & R -Seg a c= Z holds
a in Z ) implies field R c= Z )
assume A2: for a being object st a in field R & R -Seg a c= Z holds
a in Z ; :: thesis: field R c= Z
A3: now :: thesis: for a being object st a in field R & ( for b being object st [b,a] in R & a <> b holds
b in Z ) holds
a in Z
let a be object ; :: thesis: ( a in field R & ( for b being object st [b,a] in R & a <> b holds
b in Z ) implies a in Z )
assume that
A4: a in field R and
A5: for b being object st [b,a] in R & a <> b holds
b in Z ; :: thesis: a in Z
now :: thesis: for b being object st b in R -Seg a holds
b in Z
let b be object ; :: 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 A5; :: thesis: verum
end;
then R -Seg a c= Z ;
hence a in Z by A2, A4; :: thesis: verum
end;
given a being object 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 object such that
A7: a in (field R) \ Z and
A8: for b being object st b in (field R) \ Z holds
[a,b] in R by A1, Th6;
not a in Z by A7, XBOOLE_0:def 5;
then consider b being object such that
A9: [b,a] in R and
A10: b <> a and
A11: not b in Z by A3, A7;
b in field R by A9, RELAT_1:15;
then b in (field R) \ Z by A11, XBOOLE_0:def 5;
then [a,b] in R by A8;
hence contradiction by A1, A9, A10, Lm3; :: thesis: verum