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

(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

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

given a being object such that A6:
( a in field R & not a in Z )
; :: according to TARSKI:def 3 :: thesis: contradictionb 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

hence a in Z by A2, A4; :: thesis: verum

end;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

then
R -Seg a c= Z
;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;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

hence a in Z by A2, A4; :: thesis: verum

(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