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:
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 ) ) );
set W0 = bool [:(union D),(union D):];
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();
defpred S₂[ object , object ] means ex W being Relation st
( [$1,$2] in W & W in G );
consider S being Relation such that
A3: for x, y being object 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:
A4: 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 object such that
A5: ( [x,y] in R or [y,x] in R ) by Th1;
( ( 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 A3, A5;
then consider S being Relation such that
A6: ( ( [x,y] in S or [y,x] in S ) & S in G ) ;
thus x in union D by A3, A5; :: thesis:
take S ; :: thesis:
thus ( x in field S & S in G ) by A6, Th1; :: thesis:

end;

then for x being object st x in field R holds
x in union D ;
hence field R c= union D ; :: thesis:
A7: 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 that
A8: W1 in G and
A9: W2 in G ; :: thesis:
A10: W2 is well-ordering by A2, A9;
defpred S₃[ set ] means ( $1 in field W2 & W1 |_2 (W1 -Seg $1) = W2 |_2 (W2 -Seg $1) );
consider C being set such that
A11: for x being set holds
( x in C iff ( x in field W1 & S₃[x] ) ) from XFAMILY:sch 1();
A12: W1 is well-ordering by A2, A8;
A13: for x being set st x in C holds
W1 -Seg x = W2 -Seg x

proof

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

proof

let y be object ; :: thesis:
( field (W1 |_2 (W1 -Seg x)) = W1 -Seg x & field (W2 |_2 (W2 -Seg x)) = W2 -Seg x ) by A12, A10, WELLORD1:32;
hence ( y in W1 -Seg x iff y in W2 -Seg x ) by A11, A14; :: thesis:

end;

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

end;

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

proof

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

proof

let y be object ; :: thesis:
assume A17: y in W1 -Seg x ; :: thesis:
then A18: y in W2 -Seg x by A13, A16;
then A19: [y,x] in W2 by WELLORD1:1;
then A20: y in field W2 by RELAT_1:15;
A21: W1 -Seg y = (W1 |_2 (W1 -Seg x)) -Seg y by A12, A17, WELLORD1:27
.= (W2 |_2 (W2 -Seg x)) -Seg y by A11, A16
.= W2 -Seg y by A10, A18, WELLORD1:27 ;
A22: [y,x] in W1 by A17, WELLORD1:1;
then A23: y in field W1 by RELAT_1:15;
x in field W2 by A19, RELAT_1:15;
then A24: W2 -Seg y c= W2 -Seg x by A10, A18, A20, WELLORD1:30;
x in field W1 by A22, RELAT_1:15;
then W1 -Seg y c= W1 -Seg x by A12, A17, A23, WELLORD1:30;
then W1 |_2 (W1 -Seg y) = (W1 |_2 (W1 -Seg x)) |_2 (W1 -Seg y) by WELLORD1:22
.= (W2 |_2 (W2 -Seg x)) |_2 (W2 -Seg y) by A11, A16, A21
.= W2 |_2 (W2 -Seg y) by A24, WELLORD1:22 ;
hence y in C by A11, A23, A20; :: thesis:

end;

hence W1 -Seg x c= C ; :: thesis:

end;

A25: for y1 being object 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 object ; :: thesis:
set Y = (field W1) \ C;
assume ( y1 in field W1 & not y1 in C ) ; :: thesis:
then (field W1) \ C <> {} by XBOOLE_0:def 5;
then consider a being object such that
A26: a in (field W1) \ C and
A27: for b being object st b in (field W1) \ C holds
[a,b] in W1 by A12, WELLORD1:6;
take y3 = a; :: thesis:
for x being object holds
( x in C iff x in W1 -Seg y3 )

proof

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

proof

assume that
A28: x in C and
A29: not x in W1 -Seg y3 ; :: thesis:
x in field W1 by A11, A28;
then A30: [y3,x] in W1 by A12, A26, A29, Th3;
A31: W1 -Seg x c= C by A15, A28;
( y3 <> x implies y3 in C ) by A30, WELLORD1:1, A31;
hence contradiction by A26, A28, XBOOLE_0:def 5; :: thesis:

end;

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

proof

assume that
A32: x in W1 -Seg y3 and
A33: not x in C ; :: thesis:
[x,y3] in W1 by A32, WELLORD1:1;
then A34: x in field W1 by RELAT_1:15;
then x in (field W1) \ C by A33, XBOOLE_0:def 5;
then [y3,x] in W1 by A27;
hence contradiction by A12, A26, A32, A34, Th4; :: thesis:

end;

hence ( y3 is set & y3 in field W1 & C = W1 -Seg y3 & not y3 in C ) by A26, TARSKI:2, XBOOLE_0:def 5; :: thesis:

end;

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

proof

let x be set ; :: thesis:
assume A36: x in C ; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A37: y in W2 -Seg x ; :: thesis:
then A38: y in W1 -Seg x by A13, A36;
then A39: [y,x] in W1 by WELLORD1:1;
then A40: y in field W1 by RELAT_1:15;
A41: W2 -Seg y = (W2 |_2 (W2 -Seg x)) -Seg y by A10, A37, WELLORD1:27
.= (W1 |_2 (W1 -Seg x)) -Seg y by A11, A36
.= W1 -Seg y by A12, A38, WELLORD1:27 ;
A42: [y,x] in W2 by A37, WELLORD1:1;
then A43: y in field W2 by RELAT_1:15;
x in field W1 by A39, RELAT_1:15;
then A44: W1 -Seg y c= W1 -Seg x by A12, A38, A40, WELLORD1:30;
x in field W2 by A42, RELAT_1:15;
then W2 -Seg y c= W2 -Seg x by A10, A37, A43, WELLORD1:30;
then W2 |_2 (W2 -Seg y) = (W2 |_2 (W2 -Seg x)) |_2 (W2 -Seg y) by WELLORD1:22
.= (W1 |_2 (W1 -Seg x)) |_2 (W1 -Seg y) by A11, A36, A41
.= W1 |_2 (W1 -Seg y) by A44, WELLORD1:22 ;
hence y in C by A11, A43, A40; :: thesis:

end;

A45: 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:
set Y = (field W2) \ C;
assume ( y1 in field W2 & not y1 in C ) ; :: thesis:
then (field W2) \ C <> {} by XBOOLE_0:def 5;
then consider a being object such that
A46: a in (field W2) \ C and
A47: for b being object st b in (field W2) \ C holds
[a,b] in W2 by A10, WELLORD1:6;
take y3 = a; :: thesis:
for x being object holds
( x in C iff x in W2 -Seg y3 )

proof

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

proof

assume that
A48: x in C and
A49: not x in W2 -Seg y3 ; :: thesis:
x in field W2 by A11, A48;
then A50: [y3,x] in W2 by A10, A46, A49, Th3;
A51: W2 -Seg x c= C by A35, A48;
( y3 <> x implies y3 in C ) by A50, WELLORD1:1, A51;
hence contradiction by A46, A48, XBOOLE_0:def 5; :: thesis:

end;

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

proof

assume that
A52: x in W2 -Seg y3 and
A53: not x in C ; :: thesis:
[x,y3] in W2 by A52, WELLORD1:1;
then A54: x in field W2 by RELAT_1:15;
then x in (field W2) \ C by A53, XBOOLE_0:def 5;
then [y3,x] in W2 by A47;
hence contradiction by A10, A46, A52, A54, Th4; :: thesis:

end;

hence ( y3 is set & y3 in field W2 & C = W2 -Seg y3 & not y3 in C ) by A46, TARSKI:2, XBOOLE_0:def 5; :: thesis:

end;

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

proof

assume not C = field W1 ; :: thesis:
then ex x being object st
( ( x in C & not x in field W1 ) or ( x in field W1 & not x in C ) ) by TARSKI:2;
then consider y3 being set such that
A56: y3 in field W1 and
A57: C = W1 -Seg y3 and
A58: not y3 in C by A11, A25;
assume not C = field W2 ; :: thesis:
then ex x being object st
( ( x in C & not x in field W2 ) or ( x in field W2 & not x in C ) ) by TARSKI:2;
then consider y4 being set such that
A59: y4 in field W2 and
A60: C = W2 -Seg y4 and
not y4 in C by A11, A45;
A61: y3 = F . (W2 -Seg y4) by A2, A8, A56, A57, A60
.= y4 by A2, A9, A59 ;
for z being object holds
( z in W1 |_2 (W1 -Seg y3) iff z in W2 |_2 (W2 -Seg y3) )

proof

let z be object ; :: thesis:
A62: ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] implies ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] ) )

proof

assume that
A63: z in W1 and
A64: z in [:(W1 -Seg y3),(W1 -Seg y3):] ; :: thesis:
consider z1, z2 being object such that
A65: z1 in W1 -Seg y3 and
A66: z2 in W1 -Seg y3 and
A67: z = [z1,z2] by A64, ZFMISC_1:def 2;
( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A63, A67, WELLORD1:1;
then A68: ( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A13, A57, A66;
z1 in field W2 by A11, A57, A65;
hence ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] ) by A10, A57, A60, A61, A64, A67, A68, Th3, WELLORD1:1; :: thesis:

end;

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

proof

assume that
A69: z in W2 and
A70: z in [:(W2 -Seg y3),(W2 -Seg y3):] ; :: thesis:
consider z1, z2 being object such that
A71: z1 in W2 -Seg y3 and
A72: z2 in W2 -Seg y3 and
A73: z = [z1,z2] by A70, ZFMISC_1:def 2;
( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A69, A73, WELLORD1:1;
then A74: ( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A13, A60, A61, A72;
z1 in field W1 by A11, A60, A61, A71;
hence ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] ) by A12, A57, A60, A61, A70, A73, A74, Th3, WELLORD1:1; :: thesis:

end;

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

end;

then W1 |_2 (W1 -Seg y3) = W2 |_2 (W2 -Seg y3) by TARSKI:2;
hence contradiction by A11, A56, A58, A59, A61; :: thesis:

end;

A75: ( 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 A76: C = field W2 ; :: thesis:
for z1, z2 being object st [z1,z2] in W2 holds
[z1,z2] in W1

proof

let z1, z2 be object ; :: thesis:
assume A77: [z1,z2] in W2 ; :: thesis:
then A78: ( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by WELLORD1:1;
z1 in C by A76, A77, RELAT_1:15;
then A79: z1 in field W1 by A11;
z2 in C by A76, A77, RELAT_1:15;
then ( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by A13, A78;
hence [z1,z2] in W1 by A12, A79, Th3, WELLORD1:1; :: thesis:

end;

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

end;

( 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 A80: C = field W1 ; :: thesis:
for z1, z2 being object st [z1,z2] in W1 holds
[z1,z2] in W2

proof

let z1, z2 be object ; :: thesis:
assume A81: [z1,z2] in W1 ; :: thesis:
then A82: ( z1 in W1 -Seg z2 or ( z1 = z2 & not z1 in W1 -Seg z2 ) ) by WELLORD1:1;
z1 in C by A80, A81, RELAT_1:15;
then A83: z1 in field W2 by A11;
z2 in C by A80, A81, RELAT_1:15;
then ( z1 in W2 -Seg z2 or ( z1 = z2 & not z1 in W2 -Seg z2 ) ) by A13, A82;
hence [z1,z2] in W2 by A10, A83, Th3, WELLORD1:1; :: thesis:

end;

hence ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) ) by A13, A80, 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 A55, A75; :: thesis:

end;

A84: for x, y being object 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 object ; :: thesis:
assume that
x in field R and
y in field R and
A85: [x,y] in R and
A86: [y,x] in R ; :: thesis:
consider W1 being Relation such that
A87: [x,y] in W1 and
A88: W1 in G by A3, A85;
consider W2 being Relation such that
A89: [y,x] in W2 and
A90: W2 in G by A3, A86;
A91: ( W2 c= W1 implies x = y )

proof

W1 is well-ordering by A2, A88;
then W1 well_orders field W1 by WELLORD1:4;
then A92: W1 is_antisymmetric_in field W1 ;
assume A93: W2 c= W1 ; :: thesis:
then ( x in field W1 & y in field W1 ) by A89, RELAT_1:15;
hence x = y by A87, A89, A93, A92, RELAT_2:def 4; :: thesis:

end;

( W1 c= W2 implies x = y )

proof

W2 is well-ordering by A2, A90;
then W2 well_orders field W2 by WELLORD1:4;
then A94: W2 is_antisymmetric_in field W2 ;
assume A95: W1 c= W2 ; :: thesis:
then ( x in field W2 & y in field W2 ) by A87, RELAT_1:15;
hence x = y by A87, A89, A95, A94, RELAT_2:def 4; :: thesis:

end;

hence x = y by A7, A88, A90, A91; :: thesis:

end;

then A96: R is_antisymmetric_in field R by RELAT_2:def 4;
A97: for W being Relation st W in G holds
field W c= field R

proof

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

proof

assume A101: [y,x] in W ; :: thesis:
W in bool [:(union D),(union D):] by A2, A98;
then ex z1, z2 being object st
( z1 in union D & z2 in union D & [y,x] = [z1,z2] ) by A101, ZFMISC_1:84;
hence [y,x] in R by A3, A98, A101; :: thesis:

end;

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

proof

assume A102: [x,y] in W ; :: thesis:
W in bool [:(union D),(union D):] by A2, A98;
then ex z1, z2 being object st
( z1 in union D & z2 in union D & [x,y] = [z1,z2] ) by A102, ZFMISC_1:84;
hence [x,y] in R by A3, A98, A102; :: thesis:

end;

hence x in field R by A99, A100, Th1; :: thesis:

end;

A103: 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 A104: y in field R ; :: thesis:
then consider W being Relation such that
A105: y in field W and
A106: W in G by A4;
A107: y in union D by A4, A104;
A108: field W c= field R by A97, A106;
A109: for x being object st x in W -Seg y holds
x in R -Seg y

proof

let x be object ; :: thesis:
assume A110: x in W -Seg y ; :: thesis:
then A111: [x,y] in W by WELLORD1:1;
then x in field W by RELAT_1:15;
then x in union D by A4, A108;
then A112: [x,y] in R by A3, A106, A107, A111;
not x = y by A110, WELLORD1:1;
hence x in R -Seg y by A112, WELLORD1:1; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume A113: x in R -Seg y ; :: thesis:
then [x,y] in R by WELLORD1:1;
then consider W1 being Relation such that
A114: [x,y] in W1 and
A115: W1 in G by A3;
A116: y in field W1 by A114, RELAT_1:15;
not x = y by A113, WELLORD1:1;
then x in W1 -Seg y by A114, WELLORD1:1;
hence x in W -Seg y by A7, A105, A106, A115, A116; :: thesis:

end;

then W -Seg y = R -Seg y by A109, TARSKI:2;
hence ( R -Seg y in D & F . (R -Seg y) = y ) by A2, A105, A106; :: thesis:

end;

A117: for x, y being object 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 object ; :: thesis:
assume that
A118: x in field R and
A119: y in field R and
A120: x <> y ; :: thesis:
consider W2 being Relation such that
A121: y in field W2 and
A122: W2 in G by A4, A119;
consider W1 being Relation such that
A123: x in field W1 and
A124: W1 in G by A4, A118;
A125: ( x in union D & y in union D ) by A4, A118, A119;
A126: ( not W2 c= W1 or [x,y] in R or [y,x] in R )

proof

W1 is well-ordering by A2, A124;
then W1 well_orders field W1 by WELLORD1:4;
then A127: W1 is_connected_in field W1 ;
assume W2 c= W1 ; :: thesis:
then field W2 c= field W1 by RELAT_1:16;
then ( [x,y] in W1 or [y,x] in W1 ) by A120, A123, A121, A127, RELAT_2:def 6;
hence ( [x,y] in R or [y,x] in R ) by A3, A124, A125; :: thesis:

end;

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

proof

W2 is well-ordering by A2, A122;
then W2 well_orders field W2 by WELLORD1:4;
then A128: W2 is_connected_in field W2 ;
assume W1 c= W2 ; :: thesis:
then field W1 c= field W2 by RELAT_1:16;
then ( [x,y] in W2 or [y,x] in W2 ) by A120, A123, A121, A128, RELAT_2:def 6;
hence ( [x,y] in R or [y,x] in R ) by A3, A125, A122; :: thesis:

end;

hence ( [x,y] in R or [y,x] in R ) by A7, A124, A122, A126; :: thesis:

end;

then A129: R is_connected_in field R by RELAT_2:def 6;
A130: R is_well_founded_in field R

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis:
assume that
A131: Y c= field R and
A132: Y <> {} ; :: thesis:
set y = the Element of Y;
the Element of Y in field R by A131, A132;
then consider W being Relation such that
A133: the Element of Y in field W and
A134: W in G by A4;
W is well-ordering by A2, A134;
then W well_orders field W by WELLORD1:4;
then A135: W is_well_founded_in field W ;
set A = Y /\ (field W);
A136: Y /\ (field W) c= field W by XBOOLE_1:17;
Y /\ (field W) <> {} by A132, A133, XBOOLE_0:def 4;
then consider a being object such that
A137: a in Y /\ (field W) and
A138: W -Seg a misses Y /\ (field W) by A135, A136;
ex b being object st
( b in Y & R -Seg b misses Y )

proof

take b = a; :: thesis:
thus b in Y by A137, XBOOLE_0:def 4; :: thesis:
assume not R -Seg b misses Y ; :: thesis:
then consider x being object such that
A139: x in R -Seg b and
A140: x in Y by XBOOLE_0:3;
[x,b] in R by A139, WELLORD1:1;
then consider W1 being Relation such that
A141: [x,b] in W1 and
A142: W1 in G by A3;
A143: b in field W1 by A141, RELAT_1:15;
x <> b by A139, WELLORD1:1;
then x in W1 -Seg b by A141, WELLORD1:1;
then A144: x in W -Seg a by A7, A134, A136, A137, A142, A143;
then [x,a] in W by WELLORD1:1;
then x in field W by RELAT_1:15;
then x in Y /\ (field W) by A140, XBOOLE_0:def 4;
hence contradiction by A138, A144, XBOOLE_0:3; :: thesis:

end;

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

end;

A145: for x, y, z being object 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 object ; :: thesis:
assume that
x in field R and
y in field R and
z in field R and
A146: [x,y] in R and
A147: [y,z] in R ; :: thesis:
A148: ( x in union D & z in union D ) by A3, A146, A147;
consider W1 being Relation such that
A149: [x,y] in W1 and
A150: W1 in G by A3, A146;
consider W2 being Relation such that
A151: [y,z] in W2 and
A152: W2 in G by A3, A147;
ex W being Relation st
( [x,y] in W & [y,z] in W & W in G )

proof

take W = W2; :: thesis:
A153: ( not x in W1 -Seg y implies [x,y] in W )

proof

A154: W1 is well-ordering by A2, A150;
then W1 well_orders field W1 by WELLORD1:4;
then A155: W1 is_antisymmetric_in field W1 ;
W is well-ordering by A2, A152;
then W well_orders field W by WELLORD1:4;
then A156: W is_reflexive_in field W ;
A157: ( x in field W1 & y in field W1 ) by A149, RELAT_1:15;
assume not x in W1 -Seg y ; :: thesis:
then [y,x] in W1 by A157, A154, Th3;
then A158: x = y by A149, A157, A155, RELAT_2:def 4;
y in field W by A151, RELAT_1:15;
hence [x,y] in W by A158, A156, RELAT_2:def 1; :: thesis:

end;

( y in field W1 & y in field W ) by A149, A151, RELAT_1:15;
then W1 -Seg y = W -Seg y by A7, A150, A152;
hence ( [x,y] in W & [y,z] in W & W in G ) by A151, A152, A153, WELLORD1:1; :: thesis:

end;

then consider W being Relation such that
A159: [x,y] in W and
A160: [y,z] in W and
A161: W in G ;
A162: z in field W by A160, RELAT_1:15;
W is well-ordering by A2, A161;
then W well_orders field W by WELLORD1:4;
then A163: W is_transitive_in field W ;
( x in field W & y in field W ) by A159, RELAT_1:15;
then [x,z] in W by A159, A160, A163, A162, RELAT_2:def 8;
hence [x,z] in R by A3, A148, A161; :: thesis:

end;

then A164: R is_transitive_in field R by RELAT_2:def 8;
A165: for x being object st x in field R holds
[x,x] in R

proof

let x be object ; :: thesis:
assume A166: x in field R ; :: thesis:
then consider W being Relation such that
A167: x in field W and
A168: W in G by A4;
W is well-ordering by A2, A168;
then W well_orders field W by WELLORD1:4;
then W is_reflexive_in field W ;
then A169: [x,x] in W by A167, RELAT_2:def 1;
x in union D by A4, A166;
hence [x,x] in R by A3, A168, A169; :: thesis:

end;

A170: not field R in D

proof

set a0 = F . (field R);
reconsider W3 = [:(field R),{(F . (field R))}:] as Relation ;
reconsider W4 = {[(F . (field R)),(F . (field R))]} as Relation ;
reconsider W1 = (R \/ [:(field R),{(F . (field R))}:]) \/ {[(F . (field R)),(F . (field R))]} as Relation ;
( {[(F . (field R)),(F . (field R))]} c= W1 & [(F . (field R)),(F . (field R))] in {[(F . (field R)),(F . (field R))]} ) by TARSKI:def 1, XBOOLE_1:7;
then A171: F . (field R) in field W1 by RELAT_1:15;
field W4 = {(F . (field R)),(F . (field R))} by RELAT_1:17;
then A172: field W4 = {(F . (field R))} \/ {(F . (field R))} by ENUMSET1:1;
A173: ( field R = {} implies field W1 = (field R) \/ {(F . (field R))} )

proof

assume A174: field R = {} ; :: thesis:
A175: field W3 = {}

proof

set z3 = the Element of field W3;
assume field W3 <> {} ; :: thesis:
then ex z2 being object st
( [ the Element of field W3,z2] in W3 or [z2, the Element of field W3] in W3 ) by Th1;
hence contradiction by A174, ZFMISC_1:90; :: thesis:

end;

field W1 = (field (R \/ W3)) \/ (field W4) by RELAT_1:18;
then field W1 = ((field R) \/ {}) \/ {(F . (field R))} by A172, A175, RELAT_1:18;
hence field W1 = (field R) \/ {(F . (field R))} ; :: thesis:

end;

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

proof

assume field R <> {} ; :: thesis:
then A177: field W3 = (field R) \/ {(F . (field R))} by Th2;
field W1 = (field (R \/ W3)) \/ (field W4) by RELAT_1:18;
then field W1 = ((field R) \/ ((field R) \/ {(F . (field R))})) \/ {(F . (field R))} by A172, A177, RELAT_1:18;
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;

A178: 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 A176, A173, XBOOLE_0:def 3;
hence ( x in field R or x = F . (field R) ) by TARSKI:def 1; :: thesis:

end;

A179: for x, y being object 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 object ; :: 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;

for x, y being object 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 object ; :: thesis:
assume that
A180: x in field W1 and
A181: y in field W1 and
A182: x <> y ; :: thesis:
A183: ( x in field R or [x,y] in W1 or [y,x] in W1 )

proof

assume not x in field R ; :: thesis:
then A184: x = F . (field R) by A178, A180;
A185: ( 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 A184, ZFMISC_1:106;
hence ( [x,y] in W1 or [y,x] in W1 ) by A179; :: thesis:

end;

( 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 A184, TARSKI:def 1;
hence ( [x,y] in W1 or [y,x] in W1 ) by A179; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A178, A181, A185; :: thesis:

end;

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

proof

assume not y in field R ; :: thesis:
then A187: y = F . (field R) by A178, A181;
A188: ( 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 A187, ZFMISC_1:106;
hence ( [y,x] in W1 or [x,y] in W1 ) by A179; :: thesis:

end;

( 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 A187, TARSKI:def 1;
hence ( [y,x] in W1 or [x,y] in W1 ) by A179; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A178, A180, A188; :: thesis:

end;

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

proof

assume ( x in field R & y in field R ) ; :: thesis:
then ( [x,y] in R or [y,x] in R ) by A117, A182;
hence ( [x,y] in W1 or [y,x] in W1 ) by A179; :: thesis:

end;

hence ( [x,y] in W1 or [y,x] in W1 ) by A183, A186; :: thesis:

end;

then A189: W1 is_connected_in field W1 by RELAT_2:def 6;
assume A190: field R in D ; :: thesis:
for x, y being object st [x,y] in W1 holds
[x,y] in [:(union D),(union D):]

proof

let x, y be object ; :: thesis:
assume A191: [x,y] in W1 ; :: thesis:
then y in field W1 by RELAT_1:15;
then ( y in field R or y = F . (field R) ) by A178;
then A192: y in union D by A1, A4, A190;
x in field W1 by A191, RELAT_1:15;
then ( x in field R or x = F . (field R) ) by A178;
then x in union D by A1, A4, A190;
hence [x,y] in [:(union D),(union D):] by A192, ZFMISC_1:def 2; :: thesis:

end;

then A193: W1 c= [:(union D),(union D):] by RELAT_1:def 3;
A194: not F . (field R) in field R by A1, A190;
A195: for x, y being object st [x,y] in W1 & y in field R holds
( [x,y] in R & x in field R )

proof

let x, y be object ; :: thesis:
assume that
A196: [x,y] in W1 and
A197: y in field R ; :: thesis:
A198: 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 A194, A197, XTUPLE_0:1; :: thesis:

end;

not [x,y] in W3 by A194, A197, ZFMISC_1:106;
hence [x,y] in R by A179, A196, A198; :: thesis:
( [x,y] in R or [x,y] in W3 or [x,y] in W4 ) by A179, A196;
hence x in field R by A198, RELAT_1:15, ZFMISC_1:106; :: thesis:

end;

for x, y being object 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 object ; :: thesis:
assume that
A199: x in field W1 and
A200: y in field W1 and
A201: [x,y] in W1 and
A202: [y,x] in W1 ; :: thesis:
A203: ( x in field R implies x = y )

proof

assume A204: x in field R ; :: thesis:
then A205: [y,x] in R by A195, A202;
A206: y in field R by A195, A202, A204;
then [x,y] in R by A195, A201;
hence x = y by A84, A204, A205, A206; :: thesis:

end;

A207: ( y in field R implies x = y )

proof

assume A208: y in field R ; :: thesis:
then A209: [x,y] in R by A195, A201;
A210: x in field R by A195, A201, A208;
then [y,x] in R by A195, A202;
hence x = y by A84, A208, A209, A210; :: thesis:

end;

( y in field R or y = F . (field R) ) by A178, A200;
hence x = y by A178, A199, A203, A207; :: thesis:

end;

then A211: W1 is_antisymmetric_in field W1 by RELAT_2:def 4;
A212: for y being set st y in field R holds
W1 -Seg y = R -Seg y

proof

let y be set ; :: thesis:
assume A213: y in field R ; :: thesis:
A214: for x being object st x in W1 -Seg y holds
x in R -Seg y

proof

let x be object ; :: thesis:
assume A215: x in W1 -Seg y ; :: thesis:
then [x,y] in W1 by WELLORD1:1;
then A216: [x,y] in R by A195, A213;
x <> y by A215, WELLORD1:1;
hence x in R -Seg y by A216, WELLORD1:1; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume A217: x in R -Seg y ; :: thesis:
then [x,y] in R by WELLORD1:1;
then A218: [x,y] in W1 by A179;
x <> y by A217, WELLORD1:1;
hence x in W1 -Seg y by A218, WELLORD1:1; :: thesis:

end;

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

end;

A219: W1 is_well_founded_in field W1

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis:
assume that
A220: Y c= field W1 and
A221: Y <> {} ; :: thesis:
A222: ( 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:
A223: ( not (field R) /\ Y = {} implies ex a being set st
( a in Y & W1 -Seg a misses Y ) )

proof

set X = (field R) /\ Y;
A224: (field R) /\ Y c= field R by XBOOLE_1:17;
assume not (field R) /\ Y = {} ; :: thesis:
then consider y being object such that
A225: y in (field R) /\ Y and
A226: R -Seg y misses (field R) /\ Y by A130, A224;
A227: (R -Seg y) /\ Y c= (R -Seg y) /\ ((field R) /\ Y)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A228: x in (R -Seg y) /\ Y ; :: thesis:
then A229: x in Y by XBOOLE_0:def 4;
A230: x in R -Seg y by A228, XBOOLE_0:def 4;
then [x,y] in R by WELLORD1:1;
then x in field R by RELAT_1:15;
then x in (field R) /\ Y by A229, XBOOLE_0:def 4;
hence x in (R -Seg y) /\ ((field R) /\ Y) by A230, XBOOLE_0:def 4; :: thesis:

end;

(R -Seg y) /\ ((field R) /\ Y) = {} by A226, XBOOLE_0:def 7;
then (W1 -Seg y) /\ Y = {} by A212, A224, A225, A227;
then A231: W1 -Seg y misses Y by XBOOLE_0:def 7;
y in Y by A225, XBOOLE_0:def 4;
hence ex a being set st
( a in Y & W1 -Seg a misses Y ) by A231; :: thesis:

end;

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

proof

set y = the Element of Y;
A232: W1 -Seg (F . (field R)) c= field R

proof

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

end;

A235: the Element of Y in field W1 by A220, A221;
assume A236: (field R) /\ Y = {} ; :: thesis:
then not the Element of Y in field R by A221, XBOOLE_0:def 4;
then the Element of Y = F . (field R) by A178, A235;
then (W1 -Seg the Element of Y) /\ Y = {} by A236, A232, XBOOLE_1:3, XBOOLE_1:26;
then W1 -Seg the Element of Y misses Y by XBOOLE_0:def 7;
hence ex a being set st
( a in Y & W1 -Seg a misses Y ) by A221; :: thesis:

end;

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

end;

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

proof

assume A237: Y c= field R ; :: thesis:
then consider b being object such that
A238: ( b in Y & R -Seg b misses Y ) by A130, A221;
take b ; :: thesis:
thus ( b is set & b in Y & W1 -Seg b misses Y ) by A212, A237, A238; :: thesis:

end;

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

end;

A239: 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:
A240: ( y in field R implies W1 -Seg y = R -Seg y )

proof

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

proof

let x be object ; :: thesis:
A243: ( [x,y] in W4 implies [x,y] = [(F . (field R)),(F . (field R))] ) by TARSKI:def 1;
assume A244: x in W1 -Seg y ; :: thesis:
then [x,y] in W1 by WELLORD1: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;
not x = y by A244, WELLORD1:1;
hence x in R -Seg y by A194, A241, A245, A243, WELLORD1:1, XTUPLE_0:1, ZFMISC_1:106; :: thesis:

end;

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

proof

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

end;

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

end;

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

proof

let x be object ; :: thesis:
assume A249: x in W1 -Seg (F . (field R)) ; :: thesis:
then [x,(F . (field R))] in W1 by WELLORD1:1;
then A250: x in field W1 by RELAT_1:15;
not x = F . (field R) by A249, WELLORD1:1;
hence x in field R by A178, A250; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume A252: x in field R ; :: thesis:
then [x,(F . (field R))] in W3 by ZFMISC_1:106;
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 A194, A252, WELLORD1:1; :: thesis:

end;

assume y in field W1 ; :: thesis:
then ( y in field R or y = F . (field R) ) by A178;
hence ( W1 -Seg y in D & F . (W1 -Seg y) = y ) by A103, A190, A240, A248, A251, TARSKI:2; :: thesis:

end;

for x, y, z being object 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 object ; :: thesis:
assume that
A253: x in field W1 and
y in field W1 and
A254: z in field W1 and
A255: [x,y] in W1 and
A256: [y,z] in W1 ; :: thesis:
A257: ( z = F . (field R) implies [x,z] in W1 )

proof

assume A258: z = F . (field R) ; :: thesis:
A259: ( x = F . (field R) implies [x,z] in W1 )

proof

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

end;

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

proof

assume x in field R ; :: thesis:
then [x,z] in W3 by A258, ZFMISC_1:106;
hence [x,z] in W1 by A179; :: thesis:

end;

hence [x,z] in W1 by A178, A253, A259; :: thesis:

end;

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

proof

assume A260: z in field R ; :: thesis:
then A261: [y,z] in R by A195, A256;
A262: y in field R by A195, A256, A260;
then ( [x,y] in R & x in field R ) by A195, A255;
then [x,z] in R by A145, A260, A261, A262;
hence [x,z] in W1 by A179; :: thesis:

end;

hence [x,z] in W1 by A178, A254, A257; :: thesis:

end;

then A263: W1 is_transitive_in field W1 by RELAT_2:def 8;
for x being object st x in field W1 holds
[x,x] in W1

proof

let x be object ; :: thesis:
A264: ( x = F . (field R) implies [x,x] in W1 )

proof

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

end;

A266: ( x in field R implies [x,x] in W1 ) by A165, A179;
assume x in field W1 ; :: thesis:
hence [x,x] in W1 by A178, A266, A264; :: thesis:

end;

then W1 is_reflexive_in field W1 by RELAT_2:def 1;
then W1 well_orders field W1 by A263, A211, A189, A219;
then W1 is well-ordering by WELLORD1:4;
then W1 in G by A2, A193, A239;
then field W1 c= field R by A97;
hence contradiction by A1, A190, A171; :: thesis:

end;

R is_reflexive_in field R by A165, RELAT_2:def 1;
then R well_orders field R by A164, A96, A129, A130;
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 A103, A170, WELLORD1:4; :: thesis: