let F be Function; :: thesis:
let D be set ; :: thesis:
assume A1: for X being set st X in D holds
( not F . X in X & F . X in union D ) ; :: thesis:
set W0 = bool [:(union D),(union D):];
defpred S₁[ Relation] means ( $1 is well-ordering & ( for y being set st y in field $1 holds
( $1 -Seg y in D & F . ($1 -Seg y) = y ) ) );
consider G being set such that
A2: for W being Relation holds
( W in G iff ( W in bool [:(union D),(union D):] & S₁[W] ) ) from WELLSET1:sch 1();
A3: for W1, W2 being Relation st W1 in G & W2 in G & not ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) ) holds
( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) )

proof

let W1, W2 be Relation; :: thesis:
assume A4: ( W1 in G & W2 in G ) ; :: thesis:
defpred S₂[ set ] means ( $1 in field W2 & W1 |_2 (W1 -Seg $1) = W2 |_2 (W2 -Seg $1) );
consider C being set such that
A5: for x being set holds
( x in C iff ( x in field W1 & S₂[x] ) ) from XBOOLE_0:sch 1();
A6: ( W1 is well-ordering & W2 is well-ordering ) by A2, A4;
A7: for x being set st x in C holds
W1 -Seg x = W2 -Seg x

proof

let x be set ; :: thesis:
assume A8: x in C ; :: thesis:
for y being set holds
( y in W1 -Seg x iff y in W2 -Seg x )

proof

let y be set ; :: thesis:
A9: field (W1 |_2 (W1 -Seg x)) = W1 -Seg x by A6, WELLORD1:40;
field (W2 |_2 (W2 -Seg x)) = W2 -Seg x by A6, WELLORD1:40;
hence ( y in W1 -Seg x iff y in W2 -Seg x ) by A5, A8, A9; :: thesis:

end;

hence W1 -Seg x = W2 -Seg x by TARSKI:2; :: thesis:

end;

A10: for x being set st x in C holds
W1 -Seg x c= C

proof

let x be set ; :: thesis:
assume A11: x in C ; :: thesis:
for y being set st y in W1 -Seg x holds
y in C

proof

let y be set ; :: thesis:
assume A12: y in W1 -Seg x ; :: thesis:
then A13: [y,x] in W1 by WELLORD1:def 1;
then A14: y in field W1 by RELAT_1:30;
A15: x in field W1 by A13, RELAT_1:30;
then A16: W1 -Seg y c= W1 -Seg x by A6, A12, A14, WELLORD1:38;
A17: y in W2 -Seg x by A7, A11, A12;
then A18: [y,x] in W2 by WELLORD1:def 1;
then A19: y in field W2 by RELAT_1:30;
A20: x in field W2 by A18, RELAT_1:30;
then A21: W2 -Seg y c= W2 -Seg x by A6, A17, A19, WELLORD1:38;
W1 |_2 (W1 -Seg y) = W2 |_2 (W2 -Seg y)

proof

A22: W1 -Seg y = W2 -Seg y

proof

W1 -Seg y = (W1 |_2 (W1 -Seg x)) -Seg y by A6, A12, A15, WELLORD1:35
.= (W2 |_2 (W2 -Seg x)) -Seg y by A5, A11
.= W2 -Seg y by A6, A17, A20, WELLORD1:35 ;
hence W1 -Seg y = W2 -Seg y ; :: thesis:

end;

end;

hence y in C by A5, A14, A19; :: thesis:

end;

hence W1 -Seg x c= C by TARSKI:def 3; :: thesis:

end;

A23: for y1 being set st y1 in field W1 & not y1 in C holds
ex y3 being set st
( y3 in field W1 & C = W1 -Seg y3 & not y3 in C )

proof

let y1 be set ; :: thesis:
assume A24: ( y1 in field W1 & not y1 in C ) ; :: thesis:
set Y = (field W1) \ C;
(field W1) \ C <> {} by A24, XBOOLE_0:def 5;
then consider a being set such that
A25: a in (field W1) \ C and
A26: for b being set st b in (field W1) \ C holds
[a,b] in W1 by A6, WELLORD1:10;
take y3 = a; :: thesis:
C = W1 -Seg y3

proof

for x being set holds
( x in C iff x in W1 -Seg y3 )

proof

let x be set ; :: thesis:
thus ( x in C implies x in W1 -Seg y3 ) :: thesis:

proof

assume that
A27: x in C and
A28: not x in W1 -Seg y3 ; :: thesis:
x in field W1 by A5, A27;
then A29: [y3,x] in W1 by A6, A25, A28, Th6;
A30: W1 -Seg x c= C by A10, A27;
y3 in C

proof

( y3 <> x implies y3 in C )

proof

assume y3 <> x ; :: thesis:
then y3 in W1 -Seg x by A29, WELLORD1:def 1;
hence y3 in C by A30; :: thesis:

end;

hence y3 in C by A27; :: thesis:

end;

hence contradiction by A25, XBOOLE_0:def 5; :: thesis:

end;

thus ( x in W1 -Seg y3 implies x in C ) :: thesis:

proof

assume that
A31: x in W1 -Seg y3 and
A32: not x in C ; :: thesis:
[x,y3] in W1 by A31, WELLORD1:def 1;
then A33: x in field W1 by RELAT_1:30;
then x in (field W1) \ C by A32, XBOOLE_0:def 5;
then [y3,x] in W1 by A26;
hence contradiction by A6, A25, A31, A33, Th7; :: thesis:

end;

hence C = W1 -Seg y3 by TARSKI:2; :: thesis:

end;

hence ( y3 in field W1 & C = W1 -Seg y3 & not y3 in C ) by A25, XBOOLE_0:def 5; :: thesis:

end;

A34: for x being set st x in C holds
W2 -Seg x c= C

proof

let x be set ; :: thesis:
assume A35: x in C ; :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A36: y in W2 -Seg x ; :: thesis:
then A37: [y,x] in W2 by WELLORD1:def 1;
then A38: y in field W2 by RELAT_1:30;
A39: x in field W2 by A37, RELAT_1:30;
then A40: W2 -Seg y c= W2 -Seg x by A6, A36, A38, WELLORD1:38;
A41: y in W1 -Seg x by A7, A35, A36;
then A42: [y,x] in W1 by WELLORD1:def 1;
then A43: y in field W1 by RELAT_1:30;
A44: x in field W1 by A42, RELAT_1:30;
then A45: W1 -Seg y c= W1 -Seg x by A6, A41, A43, WELLORD1:38;
W2 |_2 (W2 -Seg y) = W1 |_2 (W1 -Seg y)

proof

A46: W2 -Seg y = W1 -Seg y

proof

W2 -Seg y = (W2 |_2 (W2 -Seg x)) -Seg y by A6, A36, A39, WELLORD1:35
.= (W1 |_2 (W1 -Seg x)) -Seg y by A5, A35
.= W1 -Seg y by A6, A41, A44, WELLORD1:35 ;
hence W2 -Seg y = W1 -Seg y ; :: thesis:

end;

end;

hence y in C by A5, A38, A43; :: thesis:

end;

A47: for y1 being set st y1 in field W2 & not y1 in C holds
ex y3 being set st
( y3 in field W2 & C = W2 -Seg y3 & not y3 in C )

proof

let y1 be set ; :: thesis:
assume A48: ( y1 in field W2 & not y1 in C ) ; :: thesis:
set Y = (field W2) \ C;
(field W2) \ C <> {} by A48, XBOOLE_0:def 5;
then consider a being set such that
A49: a in (field W2) \ C and
A50: for b being set st b in (field W2) \ C holds
[a,b] in W2 by A6, WELLORD1:10;
take y3 = a; :: thesis:
C = W2 -Seg y3

proof

for x being set holds
( x in C iff x in W2 -Seg y3 )

proof

let x be set ; :: thesis:
thus ( x in C implies x in W2 -Seg y3 ) :: thesis:

proof

assume that
A51: x in C and
A52: not x in W2 -Seg y3 ; :: thesis:
x in field W2 by A5, A51;
then A53: [y3,x] in W2 by A6, A49, A52, Th6;
A54: W2 -Seg x c= C by A34, A51;
( y3 <> x implies y3 in C )

proof

assume y3 <> x ; :: thesis:
then y3 in W2 -Seg x by A53, WELLORD1:def 1;
hence y3 in C by A54; :: thesis:

end;

hence contradiction by A49, A51, XBOOLE_0:def 5; :: thesis:

end;

thus ( x in W2 -Seg y3 implies x in C ) :: thesis:

proof

assume that
A55: x in W2 -Seg y3 and
A56: not x in C ; :: thesis:
[x,y3] in W2 by A55, WELLORD1:def 1;
then A57: x in field W2 by RELAT_1:30;
then x in (field W2) \ C by A56, XBOOLE_0:def 5;
then [y3,x] in W2 by A50;
hence contradiction by A6, A49, A55, A57, Th7; :: thesis:

end;

hence C = W2 -Seg y3 by TARSKI:2; :: thesis:

end;

hence ( y3 in field W2 & C = W2 -Seg y3 & not y3 in C ) by A49, XBOOLE_0:def 5; :: thesis:

end;

A58: ( C = field W1 or C = field W2 )

proof

assume not C = field W1 ; :: thesis:
then A59: ex x being set st
( ( x in C & not x in field W1 ) or ( x in field W1 & not x in C ) ) by TARSKI:2;
assume not C = field W2 ; :: thesis:
then A60: ex x being set st
( ( x in C & not x in field W2 ) or ( x in field W2 & not x in C ) ) by TARSKI:2;
consider y3 being set such that
A61: ( y3 in field W1 & C = W1 -Seg y3 & not y3 in C ) by A5, A23, A59;
consider y4 being set such that
A62: ( y4 in field W2 & C = W2 -Seg y4 & not y4 in C ) by A5, A47, A60;
A63: y3 = y4

proof

y3 = F . (W2 -Seg y4) by A2, A4, A61, A62
.= y4 by A2, A4, A62 ;
hence y3 = y4 ; :: thesis:

end;

W1 |_2 (W1 -Seg y3) = W2 |_2 (W2 -Seg y3)

proof

for z being set holds
( z in W1 |_2 (W1 -Seg y3) iff z in W2 |_2 (W2 -Seg y3) )

proof

let z be set ; :: thesis:
( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] iff ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] ) )

proof

thus ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] implies ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] ) ) :: thesis:

proof

assume that
A64: z in W1 and
A65: z in [:(W1 -Seg y3),(W1 -Seg y3):] ; :: thesis:
consider z1, z2 being set such that
A66: z1 in W1 -Seg y3 and
A67: z2 in W1 -Seg y3 and
A68: z = [z1,z2] by A65, ZFMISC_1:def 2;
A69: z1 in field W2 by A5, A61, A66;
( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A64, A68, WELLORD1:def 1;
then ( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A7, A61, A67;
hence ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] ) by A6, A61, A62, A63, A65, A68, A69, Th6, WELLORD1:def 1; :: thesis:

end;

thus ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] implies ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] ) ) :: thesis:

proof

assume that
A70: z in W2 and
A71: z in [:(W2 -Seg y3),(W2 -Seg y3):] ; :: thesis:
consider z1, z2 being set such that
A72: z1 in W2 -Seg y3 and
A73: z2 in W2 -Seg y3 and
A74: z = [z1,z2] by A71, ZFMISC_1:def 2;
A75: z1 in field W1 by A5, A62, A63, A72;
( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A70, A74, WELLORD1:def 1;
then ( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A7, A62, A63, A73;
hence ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] ) by A6, A61, A62, A63, A71, A74, A75, Th6, WELLORD1:def 1; :: thesis:

end;

hence ( z in W1 |_2 (W1 -Seg y3) iff z in W2 |_2 (W2 -Seg y3) ) by XBOOLE_0:def 4; :: thesis:

end;

hence W1 |_2 (W1 -Seg y3) = W2 |_2 (W2 -Seg y3) by TARSKI:2; :: thesis:

end;

hence contradiction by A5, A61, A62, A63; :: thesis:

end;

A76: ( C = field W1 implies ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) ) )

proof

assume A77: C = field W1 ; :: thesis:
for z1, z2 being set st [z1,z2] in W1 holds
[z1,z2] in W2

proof

let z1, z2 be set ; :: thesis:
assume A78: [z1,z2] in W1 ; :: thesis:
then A79: z1 in C by A77, RELAT_1:30;
A80: z2 in C by A77, A78, RELAT_1:30;
A81: z1 in field W2 by A5, A79;
( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A78, WELLORD1:def 1;
then ( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A7, A80;
hence [z1,z2] in W2 by A6, A81, Th6, WELLORD1:def 1; :: thesis:

end;

hence ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) ) by A7, A77, RELAT_1:def 3; :: thesis:

end;

( C = field W2 implies ( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) ) )

proof

assume A82: C = field W2 ; :: thesis:
for z1, z2 being set st [z1,z2] in W2 holds
[z1,z2] in W1

proof

let z1, z2 be set ; :: thesis:
assume A83: [z1,z2] in W2 ; :: thesis:
then A84: z1 in C by A82, RELAT_1:30;
A85: z2 in C by A82, A83, RELAT_1:30;
A86: z1 in field W1 by A5, A84;
( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A83, WELLORD1:def 1;
then ( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A7, A85;
hence [z1,z2] in W1 by A6, A86, Th6, WELLORD1:def 1; :: thesis:

end;

hence ( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) ) by A7, A82, RELAT_1:def 3; :: thesis:

end;

hence ( ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) ) or ( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) ) ) by A58, A76; :: thesis:

end;

defpred S₂[ set , set ] means ex W being Relation st
( [$1,$2] in W & W in G );
consider S being Relation such that
A87: for x, y being set holds
( [x,y] in S iff ( x in union D & y in union D & S₂[x,y] ) ) from RELAT_1:sch 1();
take R = S; :: thesis:
A88: for x being set st x in field R holds
( x in union D & ex W being Relation st
( x in field W & W in G ) )

proof

let x be set ; :: thesis:
assume x in field R ; :: thesis:
then consider y being set such that
A89: ( [x,y] in R or [y,x] in R ) by Th1;
A90: ( ( x in union D & y in union D & ex S being Relation st
( [x,y] in S & S in G ) ) or ( y in union D & x in union D & ex S being Relation st
( [y,x] in S & S in G ) ) ) by A87, A89;
thus x in union D by A87, A89; :: thesis:
consider S being Relation such that
A91: ( [x,y] in S or [y,x] in S ) and
A92: S in G by A90;
take S ; :: thesis:
thus ( x in field S & S in G ) by A91, A92, Th1; :: thesis:

end;

then for x being set st x in field R holds
x in union D ;
hence field R c= union D by TARSKI:def 3; :: thesis:
A93: for W being Relation st W in G holds
field W c= field R

proof

let W be Relation; :: thesis:
assume A94: W in G ; :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in field W ; :: thesis:
then consider y being set such that
A95: ( [x,y] in W or [y,x] in W ) by Th1;
A96: ( [x,y] in W implies [x,y] in R )

proof

assume A97: [x,y] in W ; :: thesis:
W in bool [:(union D),(union D):] by A2, A94;
then ex z1, z2 being set st
( z1 in union D & z2 in union D & [x,y] = [z1,z2] ) by A97, ZFMISC_1:103;
hence [x,y] in R by A87, A94, A97; :: thesis:

end;

( [y,x] in W implies [y,x] in R )

proof

assume A98: [y,x] in W ; :: thesis:
W in bool [:(union D),(union D):] by A2, A94;
then ex z1, z2 being set st
( z1 in union D & z2 in union D & [y,x] = [z1,z2] ) by A98, ZFMISC_1:103;
hence [y,x] in R by A87, A94, A98; :: thesis:

end;

hence x in field R by A95, A96, Th1; :: thesis:

end;

A99: R is well-ordering

proof

A100: R is_reflexive_in field R

proof

for x being set st x in field R holds
[x,x] in R

proof

let x be set ; :: thesis:
assume A101: x in field R ; :: thesis:
then A102: ( x in union D & ex W being Relation st
( x in field W & W in G ) ) by A88;
consider W being Relation such that
A103: ( x in field W & W in G ) by A88, A101;
W is well-ordering by A2, A103;
then W well_orders field W by WELLORD1:8;
then W is_reflexive_in field W by WELLORD1:def 5;
then [x,x] in W by A103, RELAT_2:def 1;
hence [x,x] in R by A87, A102, A103; :: thesis:

end;

hence R is_reflexive_in field R by RELAT_2:def 1; :: thesis:

end;

A104: R is_transitive_in field R

proof

for x, y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R

proof

let x, y, z be set ; :: thesis:
assume that
x in field R and
y in field R and
z in field R and
A105: ( [x,y] in R & [y,z] in R ) ; :: thesis:
A106: ( x in union D & y in union D & ex W being Relation st
( [x,y] in W & W in G ) ) by A87, A105;
consider W1 being Relation such that
A107: ( [x,y] in W1 & W1 in G ) by A87, A105;
A108: ( y in union D & z in union D & ex W being Relation st
( [y,z] in W & W in G ) ) by A87, A105;
consider W2 being Relation such that
A109: ( [y,z] in W2 & W2 in G ) by A87, A105;
ex W being Relation st
( [x,y] in W & [y,z] in W & W in G )

proof

take W = W2; :: thesis:
( y in field W1 & y in field W ) by A107, A109, RELAT_1:30;
then A110: W1 -Seg y = W -Seg y by A3, A107, A109;
( not x in W1 -Seg y implies [x,y] in W )

proof

assume A111: not x in W1 -Seg y ; :: thesis:
A112: ( x in field W1 & y in field W1 ) by A107, RELAT_1:30;
A113: W1 is well-ordering by A2, A107;
then A114: [y,x] in W1 by A111, A112, Th6;
W1 well_orders field W1 by A113, WELLORD1:8;
then W1 is_antisymmetric_in field W1 by WELLORD1:def 5;
then A115: x = y by A107, A112, A114, RELAT_2:def 4;
A116: y in field W by A109, RELAT_1:30;
W is well-ordering by A2, A109;
then W well_orders field W by WELLORD1:8;
then W is_reflexive_in field W by WELLORD1:def 5;
hence [x,y] in W by A115, A116, RELAT_2:def 1; :: thesis:

end;

hence ( [x,y] in W & [y,z] in W & W in G ) by A109, A110, WELLORD1:def 1; :: thesis:

end;

then consider W being Relation such that
A117: ( [x,y] in W & [y,z] in W & W in G ) ;
W is well-ordering by A2, A117;
then W well_orders field W by WELLORD1:8;
then A118: W is_transitive_in field W by WELLORD1:def 5;
( x in field W & y in field W & z in field W ) by A117, RELAT_1:30;
then [x,z] in W by A117, A118, RELAT_2:def 8;
hence [x,z] in R by A87, A106, A108, A117; :: thesis:

end;

hence R is_transitive_in field R by RELAT_2:def 8; :: thesis:

end;

A119: R is_antisymmetric_in field R

proof

for x, y being set st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y

proof

let x, y be set ; :: thesis:
assume that
x in field R and
y in field R and
A120: ( [x,y] in R & [y,x] in R ) ; :: thesis:
consider W1 being Relation such that
A121: ( [x,y] in W1 & W1 in G ) by A87, A120;
consider W2 being Relation such that
A122: ( [y,x] in W2 & W2 in G ) by A87, A120;
A123: ( W1 c= W2 implies x = y )

proof

assume A124: W1 c= W2 ; :: thesis:
then A125: ( x in field W2 & y in field W2 ) by A121, RELAT_1:30;
W2 is well-ordering by A2, A122;
then W2 well_orders field W2 by WELLORD1:8;
then W2 is_antisymmetric_in field W2 by WELLORD1:def 5;
hence x = y by A121, A122, A124, A125, RELAT_2:def 4; :: thesis:

end;

( W2 c= W1 implies x = y )

proof

assume A126: W2 c= W1 ; :: thesis:
then A127: ( x in field W1 & y in field W1 ) by A122, RELAT_1:30;
W1 is well-ordering by A2, A121;
then W1 well_orders field W1 by WELLORD1:8;
then W1 is_antisymmetric_in field W1 by WELLORD1:def 5;
hence x = y by A121, A122, A126, A127, RELAT_2:def 4; :: thesis:

end;

hence x = y by A3, A121, A122, A123; :: thesis:

end;

hence R is_antisymmetric_in field R by RELAT_2:def 4; :: thesis:

end;

A128: R is_connected_in field R

proof

for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R

proof

let x, y be set ; :: thesis:
assume that
A129: x in field R and
A130: y in field R and
A131: x <> y ; :: thesis:
A132: ( x in union D & ex W being Relation st
( x in field W & W in G ) ) by A88, A129;
consider W1 being Relation such that
A133: ( x in field W1 & W1 in G ) by A88, A129;
A134: ( y in union D & ex W being Relation st
( y in field W & W in G ) ) by A88, A130;
consider W2 being Relation such that
A135: ( y in field W2 & W2 in G ) by A88, A130;
A136: ( not W1 c= W2 or [x,y] in R or [y,x] in R )

proof

assume W1 c= W2 ; :: thesis:
then A137: field W1 c= field W2 by RELAT_1:31;
W2 is well-ordering by A2, A135;
then W2 well_orders field W2 by WELLORD1:8;
then W2 is_connected_in field W2 by WELLORD1:def 5;
then ( [x,y] in W2 or [y,x] in W2 ) by A131, A133, A135, A137, RELAT_2:def 6;
hence ( [x,y] in R or [y,x] in R ) by A87, A132, A134, A135; :: thesis:

end;

( not W2 c= W1 or [x,y] in R or [y,x] in R )

proof

assume W2 c= W1 ; :: thesis:
then A138: field W2 c= field W1 by RELAT_1:31;
W1 is well-ordering by A2, A133;
then W1 well_orders field W1 by WELLORD1:8;
then W1 is_connected_in field W1 by WELLORD1:def 5;
then ( [x,y] in W1 or [y,x] in W1 ) by A131, A133, A135, A138, RELAT_2:def 6;
hence ( [x,y] in R or [y,x] in R ) by A87, A132, A133, A134; :: thesis:

end;

hence ( [x,y] in R or [y,x] in R ) by A3, A133, A135, A136; :: thesis:

end;

hence R is_connected_in field R by RELAT_2:def 6; :: thesis:

end;

R is_well_founded_in field R

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis:
assume that
A139: Y c= field R and
A140: Y <> {} ; :: thesis:
consider y being Element of Y;
y in field R by A139, A140, TARSKI:def 3;
then consider W being Relation such that
A141: ( y in field W & W in G ) by A88;
W is well-ordering by A2, A141;
then W well_orders field W by WELLORD1:8;
then A142: W is_well_founded_in field W by WELLORD1:def 5;
set A = Y /\ (field W);
A143: Y /\ (field W) c= field W by XBOOLE_1:17;
Y /\ (field W) <> {} by A140, A141, XBOOLE_0:def 4;
then consider a being set such that
A144: a in Y /\ (field W) and
A145: W -Seg a misses Y /\ (field W) by A142, A143, WELLORD1:def 3;
ex b being set st
( b in Y & R -Seg b misses Y )

proof

take b = a; :: thesis:
thus b in Y by A144, XBOOLE_0:def 4; :: thesis:
assume not R -Seg b misses Y ; :: thesis:
then consider x being set such that
A146: ( x in R -Seg b & x in Y ) by XBOOLE_0:3;
A147: ( [x,b] in R & x <> b ) by A146, WELLORD1:def 1;
then consider W1 being Relation such that
A148: ( [x,b] in W1 & W1 in G ) by A87;
A149: ( x in field W1 & b in field W1 ) by A148, RELAT_1:30;
x in W1 -Seg b by A147, A148, WELLORD1:def 1;
then A150: x in W -Seg a by A3, A141, A143, A144, A148, A149;
then [x,a] in W by WELLORD1:def 1;
then x in field W by RELAT_1:30;
then x in Y /\ (field W) by A146, XBOOLE_0:def 4;
hence contradiction by A145, A150, XBOOLE_0:3; :: thesis:

end;

hence ex b₁ being set st
( b₁ in Y & R -Seg b₁ misses Y ) ; :: thesis:

end;

then R well_orders field R by A100, A104, A119, A128, WELLORD1:def 5;
hence R is well-ordering by WELLORD1:8; :: thesis:

end;

A151: for y being set st y in field R holds
( R -Seg y in D & F . (R -Seg y) = y )

proof

let y be set ; :: thesis:
assume A152: y in field R ; :: thesis:
then consider W being Relation such that
A153: ( y in field W & W in G ) by A88;
A154: y in union D by A88, A152;
A155: field W c= field R by A93, A153;
W -Seg y = R -Seg y

proof

A156: for x being set st x in W -Seg y holds
x in R -Seg y

proof

let x be set ; :: thesis:
assume x in W -Seg y ; :: thesis:
then A157: ( [x,y] in W & not x = y ) by WELLORD1:def 1;
then x in field W by RELAT_1:30;
then x in union D by A88, A155;
then [x,y] in R by A87, A153, A154, A157;
hence x in R -Seg y by A157, WELLORD1:def 1; :: thesis:

end;

for x being set st x in R -Seg y holds
x in W -Seg y

proof

let x be set ; :: thesis:
assume x in R -Seg y ; :: thesis:
then A158: ( [x,y] in R & not x = y ) by WELLORD1:def 1;
then consider W1 being Relation such that
A159: ( [x,y] in W1 & W1 in G ) by A87;
A160: x in W1 -Seg y by A158, A159, WELLORD1:def 1;
y in field W1 by A159, RELAT_1:30;
hence x in W -Seg y by A3, A153, A159, A160; :: thesis:

end;

hence W -Seg y = R -Seg y by A156, TARSKI:2; :: thesis:

end;

hence ( R -Seg y in D & F . (R -Seg y) = y ) by A2, A153; :: thesis:

end;

not field R in D

proof

assume A161: field R in D ; :: thesis:
set a0 = F . (field R);
A162: not F . (field R) in field R by A1, A161;
reconsider W3 = [:(field R),{(F . (field R))}:] as Relation ;
reconsider W4 = {[(F . (field R)),(F . (field R))]} as Relation ;
field W4 = {(F . (field R)),(F . (field R))} by RELAT_1:32;
then A163: field W4 = {(F . (field R))} \/ {(F . (field R))} by ENUMSET1:41;
reconsider W1 = (R \/ [:(field R),{(F . (field R))}:]) \/ {[(F . (field R)),(F . (field R))]} as Relation ;
A164: field W1 = (field R) \/ {(F . (field R))}

proof

A165: ( field R <> {} implies field W1 = (field R) \/ {(F . (field R))} )

proof

assume field R <> {} ; :: thesis:
then A166: field W3 = (field R) \/ {(F . (field R))} by Th3;
field W1 = (field (R \/ W3)) \/ (field W4) by RELAT_1:33;
then field W1 = ((field R) \/ ((field R) \/ {(F . (field R))})) \/ {(F . (field R))} by A163, A166, RELAT_1:33;
then field W1 = (((field R) \/ (field R)) \/ {(F . (field R))}) \/ {(F . (field R))} by XBOOLE_1:4;
then field W1 = ((field R) \/ (field R)) \/ ({(F . (field R))} \/ {(F . (field R))}) by XBOOLE_1:4;
hence field W1 = (field R) \/ {(F . (field R))} ; :: thesis:

end;

( field R = {} implies field W1 = (field R) \/ {(F . (field R))} )

proof

assume A167: field R = {} ; :: thesis:
A168: field W3 = {}

proof

consider z3 being Element of field W3;
assume field W3 <> {} ; :: thesis:
then ex z2 being set st
( [z3,z2] in W3 or [z2,z3] in W3 ) by Th1;
hence contradiction by A167, ZFMISC_1:113; :: thesis:

end;

field W1 = (field (R \/ W3)) \/ (field W4) by RELAT_1:33;
then field W1 = ((field R) \/ {} ) \/ {(F . (field R))} by A163, A168, RELAT_1:33;
hence field W1 = (field R) \/ {(F . (field R))} ; :: thesis:

end;

hence field W1 = (field R) \/ {(F . (field R))} by A165; :: thesis:

end;

A169: for x being set holds
( not x in field W1 or x in field R or x = F . (field R) )

proof

let x be set ; :: thesis:
assume x in field W1 ; :: thesis:
then ( x in field R or x in {(F . (field R))} ) by A164, XBOOLE_0:def 3;
hence ( x in field R or x = F . (field R) ) by TARSKI:def 1; :: thesis:

end;

A170: for x, y being set holds
( [x,y] in W1 iff ( [x,y] in R or [x,y] in W3 or [x,y] in W4 ) )

proof

let x, y be set ; :: thesis:
( [x,y] in W1 iff ( [x,y] in R \/ W3 or [x,y] in W4 ) ) by XBOOLE_0:def 3;
hence ( [x,y] in W1 iff ( [x,y] in R or [x,y] in W3 or [x,y] in W4 ) ) by XBOOLE_0:def 3; :: thesis:

end;

A171: for x, y being set st [x,y] in W1 & y in field R holds
( [x,y] in R & x in field R )

proof

let x, y be set ; :: thesis:
assume A172: ( [x,y] in W1 & y in field R ) ; :: thesis:
then A173: ( [x,y] in R or [x,y] in W3 or [x,y] in W4 ) by A170;
A174: not [x,y] in W3 by A162, A172, ZFMISC_1:129;
A175: not [x,y] in W4

proof

assume [x,y] in W4 ; :: thesis:
then [x,y] = [(F . (field R)),(F . (field R))] by TARSKI:def 1;
hence contradiction by A162, A172, ZFMISC_1:33; :: thesis:

end;

hence [x,y] in R by A170, A172, A174; :: thesis:
thus x in field R by A173, A175, RELAT_1:30, ZFMISC_1:129; :: thesis:

end;

A176: for y being set st y in field R holds
W1 -Seg y = R -Seg y

proof

let y be set ; :: thesis:
assume A177: y in field R ; :: thesis:
A178: for x being set st x in W1 -Seg y holds
x in R -Seg y

proof

let x be set ; :: thesis:
assume x in W1 -Seg y ; :: thesis:
then A179: ( [x,y] in W1 & x <> y ) by WELLORD1:def 1;
then [x,y] in R by A171, A177;
hence x in R -Seg y by A179, WELLORD1:def 1; :: thesis:

end;

for x being set st x in R -Seg y holds
x in W1 -Seg y

proof

let x be set ; :: thesis:
assume x in R -Seg y ; :: thesis:
then A180: ( [x,y] in R & x <> y ) by WELLORD1:def 1;
then [x,y] in W1 by A170;
hence x in W1 -Seg y by A180, WELLORD1:def 1; :: thesis:

end;

hence W1 -Seg y = R -Seg y by A178, TARSKI:2; :: thesis:

end;

A181: W1 in bool [:(union D),(union D):]

proof

for x, y being set st [x,y] in W1 holds
[x,y] in [:(union D),(union D):]

proof

let x, y be set ; :: thesis:
assume [x,y] in W1 ; :: thesis:
then ( x in field W1 & y in field W1 ) by RELAT_1:30;
then ( ( x in field R or x = F . (field R) ) & ( y in field R or y = F . (field R) ) ) by A169;
then ( x in union D & y in union D ) by A1, A88, A161;
hence [x,y] in [:(union D),(union D):] by ZFMISC_1:def 2; :: thesis:

end;

then W1 c= [:(union D),(union D):] by RELAT_1:def 3;
hence W1 in bool [:(union D),(union D):] ; :: thesis:

end;

A182: W1 is well-ordering

proof

A183: W1 is_reflexive_in field W1

proof

for x being set st x in field W1 holds
[x,x] in W1

proof

let x be set ; :: thesis:
assume A184: x in field W1 ; :: thesis:
A185: ( x in field R implies [x,x] in W1 )

proof

assume A186: x in field R ; :: thesis:
R well_orders field R by A99, WELLORD1:8;
then R is_reflexive_in field R by WELLORD1:def 5;
then [x,x] in R by A186, RELAT_2:def 1;
hence [x,x] in W1 by A170; :: thesis:

end;

( x = F . (field R) implies [x,x] in W1 )

proof

assume A187: x = F . (field R) ; :: thesis:
[(F . (field R)),(F . (field R))] in W4 by TARSKI:def 1;
hence [x,x] in W1 by A170, A187; :: thesis:

end;

hence [x,x] in W1 by A169, A184, A185; :: thesis:

end;

hence W1 is_reflexive_in field W1 by RELAT_2:def 1; :: thesis:

end;

A188: W1 is_transitive_in field W1

proof

for x, y, z being set st x in field W1 & y in field W1 & z in field W1 & [x,y] in W1 & [y,z] in W1 holds
[x,z] in W1

proof

let x, y, z be set ; :: thesis:
assume that
A189: x in field W1 and
A190: y in field W1 and
A191: z in field W1 and
A192: ( [x,y] in W1 & [y,z] in W1 ) ; :: thesis:
A193: ( z in field R implies [x,z] in W1 )

proof

assume A194: z in field R ; :: thesis:
then A195: ( [y,z] in R & y in field R ) by A171, A192;
then A196: ( [x,y] in R & x in field R ) by A171, A192;
R well_orders field R by A99, WELLORD1:8;
then R is_transitive_in field R by WELLORD1:def 5;
then [x,z] in R by A194, A195, A196, RELAT_2:def 8;
hence [x,z] in W1 by A170; :: thesis:

end;

( z = F . (field R) implies [x,z] in W1 )

proof

assume A197: z = F . (field R) ; :: thesis:
A198: ( y in field R implies [x,z] in W1 )

proof

assume y in field R ; :: thesis:
then ( [x,y] in R & x in field R ) by A171, A192;
then [x,z] in W3 by A197, ZFMISC_1:129;
hence [x,z] in W1 by A170; :: thesis:

end;

( y = F . (field R) implies [x,z] in W1 )

proof

A199: ( x in field R implies [x,z] in W1 )

proof

assume x in field R ; :: thesis:
then [x,z] in W3 by A197, ZFMISC_1:129;
hence [x,z] in W1 by A170; :: thesis:

end;

( x = F . (field R) implies [x,z] in W1 )

proof

assume x = F . (field R) ; :: thesis:
then [x,z] in W4 by A197, TARSKI:def 1;
hence [x,z] in W1 by A170; :: thesis:

end;

hence ( y = F . (field R) implies [x,z] in W1 ) by A169, A189, A199; :: thesis:

end;

hence [x,z] in W1 by A169, A190, A198; :: thesis:

end;

hence [x,z] in W1 by A169, A191, A193; :: thesis:

end;

hence W1 is_transitive_in field W1 by RELAT_2:def 8; :: thesis:

end;

A200: W1 is_antisymmetric_in field W1

proof

for x, y being set st x in field W1 & y in field W1 & [x,y] in W1 & [y,x] in W1 holds
x = y

proof

let x, y be set ; :: thesis:
assume that
A201: x in field W1 and
A202: y in field W1 and
A203: ( [x,y] in W1 & [y,x] in W1 ) ; :: thesis:
A204: ( y in field R or y = F . (field R) ) by A169, A202;
A205: ( x in field R implies x = y )

proof

assume A206: x in field R ; :: thesis:
then A207: ( [y,x] in R & y in field R ) by A171, A203;
then A208: [x,y] in R by A171, A203;
R well_orders field R by A99, WELLORD1:8;
then R is_antisymmetric_in field R by WELLORD1:def 5;
hence x = y by A206, A207, A208, RELAT_2:def 4; :: thesis:

end;

( y in field R implies x = y )

proof

assume A209: y in field R ; :: thesis:
then A210: ( [x,y] in R & x in field R ) by A171, A203;
then A211: [y,x] in R by A171, A203;
R well_orders field R by A99, WELLORD1:8;
then R is_antisymmetric_in field R by WELLORD1:def 5;
hence x = y by A209, A210, A211, RELAT_2:def 4; :: thesis:

end;

hence x = y by A169, A201, A204, A205; :: thesis:

end;

hence W1 is_antisymmetric_in field W1 by RELAT_2:def 4; :: thesis:

end;

A212: W1 is_connected_in field W1

proof

for x, y being set st x in field W1 & y in field W1 & x <> y & not [x,y] in W1 holds
[y,x] in W1

proof

let x, y be set ; :: thesis:
assume that
A213: x in field W1 and
A214: y in field W1 and
A215: x <> y ; :: thesis:
A216: ( x in field R & y in field R & not [x,y] in W1 implies [y,x] in W1 )

proof

assume A217: ( x in field R & y in field R ) ; :: thesis:
R well_orders field R by A99, WELLORD1:8;
then R is_connected_in field R by WELLORD1:def 5;
then ( [x,y] in R or [y,x] in R ) by A215, A217, RELAT_2:def 6;
hence ( [x,y] in W1 or [y,x] in W1 ) by A170; :: thesis:

end;

A218: ( x in field R or [x,y] in W1 or [y,x] in W1 )

proof

assume not x in field R ; :: thesis:
then A219: x = F . (field R) by A169, A213;
A220: ( not y = F . (field R) or [x,y] in W1 or [y,x] in W1 )

proof

assume y = F . (field R) ; :: thesis:
then [x,y] in W4 by A219, TARSKI:def 1;
hence ( [x,y] in W1 or [y,x] in W1 ) by A170; :: thesis:

end;

( not y in field R or [x,y] in W1 or [y,x] in W1 )

proof

assume y in field R ; :: thesis:
then [y,x] in W3 by A219, ZFMISC_1:129;
hence ( [x,y] in W1 or [y,x] in W1 ) by A170; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A169, A214, A220; :: thesis:

end;

( y in field R or [x,y] in W1 or [y,x] in W1 )

proof

assume not y in field R ; :: thesis:
then A221: y = F . (field R) by A169, A214;
A222: ( not x = F . (field R) or [y,x] in W1 or [x,y] in W1 )

proof

assume x = F . (field R) ; :: thesis:
then [y,x] in W4 by A221, TARSKI:def 1;
hence ( [y,x] in W1 or [x,y] in W1 ) by A170; :: thesis:

end;

( not x in field R or [y,x] in W1 or [x,y] in W1 )

proof

assume x in field R ; :: thesis:
then [x,y] in W3 by A221, ZFMISC_1:129;
hence ( [y,x] in W1 or [x,y] in W1 ) by A170; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A169, A213, A222; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A216, A218; :: thesis:

end;

hence W1 is_connected_in field W1 by RELAT_2:def 6; :: thesis:

end;

W1 is_well_founded_in field W1

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis:
assume that
A223: Y c= field W1 and
A224: Y <> {} ; :: thesis:
R well_orders field R by A99, WELLORD1:8;
then A225: R is_well_founded_in field R by WELLORD1:def 5;
A226: ( Y c= field R implies ex a being set st
( a in Y & W1 -Seg a misses Y ) )

proof

assume A227: Y c= field R ; :: thesis:
then consider b being set such that
A228: ( b in Y & R -Seg b misses Y ) by A224, A225, WELLORD1:def 3;
take b ; :: thesis:
thus ( b in Y & W1 -Seg b misses Y ) by A176, A227, A228; :: thesis:

end;

( not Y c= field R implies ex a being set st
( a in Y & W1 -Seg a misses Y ) )

proof

assume not Y c= field R ; :: thesis:
A229: ( (field R) /\ Y = {} implies ex a being set st
( a in Y & W1 -Seg a misses Y ) )

proof

assume A230: (field R) /\ Y = {} ; :: thesis:
consider y being Element of Y;
A231: not y in field R by A224, A230, XBOOLE_0:def 4;
y in field W1 by A223, A224, TARSKI:def 3;
then A232: y = F . (field R) by A169, A231;
W1 -Seg (F . (field R)) c= field R

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in W1 -Seg (F . (field R)) ; :: thesis:
then A233: ( [z,(F . (field R))] in W1 & z <> F . (field R) ) by WELLORD1:def 1;
then z in field W1 by RELAT_1:30;
hence z in field R by A169, A233; :: thesis:

end;

then (W1 -Seg y) /\ Y = {} by A230, A232, XBOOLE_1:3, XBOOLE_1:26;
then W1 -Seg y misses Y by XBOOLE_0:def 7;
hence ex a being set st
( a in Y & W1 -Seg a misses Y ) by A224; :: thesis:

end;

( not (field R) /\ Y = {} implies ex a being set st
( a in Y & W1 -Seg a misses Y ) )

proof

assume A234: not (field R) /\ Y = {} ; :: thesis:
set X = (field R) /\ Y;
A235: (field R) /\ Y c= field R by XBOOLE_1:17;
then consider y being set such that
A236: ( y in (field R) /\ Y & R -Seg y misses (field R) /\ Y ) by A225, A234, WELLORD1:def 3;
A237: y in Y by A236, XBOOLE_0:def 4;
A238: (R -Seg y) /\ ((field R) /\ Y) = {} by A236, XBOOLE_0:def 7;
(R -Seg y) /\ Y c= (R -Seg y) /\ ((field R) /\ Y)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (R -Seg y) /\ Y ; :: thesis:
then A239: ( x in R -Seg y & x in Y ) by XBOOLE_0:def 4;
then [x,y] in R by WELLORD1:def 1;
then x in field R by RELAT_1:30;
then x in (field R) /\ Y by A239, XBOOLE_0:def 4;
hence x in (R -Seg y) /\ ((field R) /\ Y) by A239, XBOOLE_0:def 4; :: thesis:

end;

then (R -Seg y) /\ Y = {} by A238;
then (W1 -Seg y) /\ Y = {} by A176, A235, A236;
then W1 -Seg y misses Y by XBOOLE_0:def 7;
hence ex a being set st
( a in Y & W1 -Seg a misses Y ) by A237; :: thesis:

end;

hence ex a being set st
( a in Y & W1 -Seg a misses Y ) by A229; :: thesis:

end;

hence ex b₁ being set st
( b₁ in Y & W1 -Seg b₁ misses Y ) by A226; :: thesis:

end;

then W1 well_orders field W1 by A183, A188, A200, A212, WELLORD1:def 5;
hence W1 is well-ordering by WELLORD1:8; :: thesis:

end;

for y being set st y in field W1 holds
( W1 -Seg y in D & F . (W1 -Seg y) = y )

proof

let y be set ; :: thesis:
assume y in field W1 ; :: thesis:
then A240: ( y in field R or y = F . (field R) ) by A169;
A241: ( y in field R implies W1 -Seg y = R -Seg y )

proof

assume A242: y in field R ; :: thesis:
A243: for x being set st x in W1 -Seg y holds
x in R -Seg y

proof

let x be set ; :: thesis:
assume x in W1 -Seg y ; :: thesis:
then A244: ( [x,y] in W1 & not x = y ) by WELLORD1:def 1;
then ( [x,y] in R \/ W3 or [x,y] in W4 ) by XBOOLE_0:def 3;
then A245: ( [x,y] in R or [x,y] in W3 or [x,y] in W4 ) by XBOOLE_0:def 3;
( [x,y] in W4 implies [x,y] = [(F . (field R)),(F . (field R))] ) by TARSKI:def 1;
hence x in R -Seg y by A162, A242, A244, A245, WELLORD1:def 1, ZFMISC_1:33, ZFMISC_1:129; :: thesis:

end;

for x being set st x in R -Seg y holds
x in W1 -Seg y

proof

let x be set ; :: thesis:
assume x in R -Seg y ; :: thesis:
then A246: ( [x,y] in R & not x = y ) by WELLORD1:def 1;
then [x,y] in R \/ W3 by XBOOLE_0:def 3;
then [x,y] in W1 by XBOOLE_0:def 3;
hence x in W1 -Seg y by A246, WELLORD1:def 1; :: thesis:

end;

hence W1 -Seg y = R -Seg y by A243, TARSKI:2; :: thesis:

end;

( W1 -Seg (F . (field R)) in D & F . (W1 -Seg (F . (field R))) = F . (field R) )

proof

W1 -Seg (F . (field R)) = field R

proof

A247: for x being set st x in W1 -Seg (F . (field R)) holds
x in field R

proof

let x be set ; :: thesis:
assume x in W1 -Seg (F . (field R)) ; :: thesis:
then A248: ( [x,(F . (field R))] in W1 & not x = F . (field R) ) by WELLORD1:def 1;
then x in field W1 by RELAT_1:30;
hence x in field R by A169, A248; :: thesis:

end;

for x being set st x in field R holds
x in W1 -Seg (F . (field R))

proof

let x be set ; :: thesis:
assume A249: x in field R ; :: thesis:
then [x,(F . (field R))] in W3 by ZFMISC_1:129;
then [x,(F . (field R))] in R \/ W3 by XBOOLE_0:def 3;
then [x,(F . (field R))] in W1 by XBOOLE_0:def 3;
hence x in W1 -Seg (F . (field R)) by A162, A249, WELLORD1:def 1; :: thesis:

end;

hence W1 -Seg (F . (field R)) = field R by A247, TARSKI:2; :: thesis:

end;

hence ( W1 -Seg (F . (field R)) in D & F . (W1 -Seg (F . (field R))) = F . (field R) ) by A161; :: thesis:

end;

hence ( W1 -Seg y in D & F . (W1 -Seg y) = y ) by A151, A240, A241; :: thesis:

end;

then W1 in G by A2, A181, A182;
then A250: field W1 c= field R by A93;
A251: {[(F . (field R)),(F . (field R))]} c= W1 by XBOOLE_1:7;
[(F . (field R)),(F . (field R))] in {[(F . (field R)),(F . (field R))]} by TARSKI:def 1;
then F . (field R) in field W1 by A251, RELAT_1:30;
hence contradiction by A1, A161, A250; :: thesis:

end;

hence ( R is well-ordering & not field R in D & ( for y being set st y in field R holds
( R -Seg y in D & F . (R -Seg y) = y ) ) ) by A99, A151; :: thesis: