:: WELLSET1 semantic presentation

begin


theorem Th1: :: WELLSET1:1
for x being set
for R being Relation holds
( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) )
proof
let x be set ; ::_thesis: for R being Relation holds
( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) )
let R be Relation; ::_thesis: ( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) )
 ( x in (dom R) \/ (rng R) iff ( x in dom R or x in rng R ) ) by XBOOLE_0:def_3;
hence  ( x in field R iff ex y being set st
( [x,y] in R or [y,x] in R ) ) by RELAT_1:def_6, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th2: :: WELLSET1:2
for X, Y being set
for W being Relation st X <> {} & Y <> {} & W = [:X,Y:] holds
field W = X \/ Y
proof
let X, Y be set ; ::_thesis: for W being Relation st X <> {} & Y <> {} & W = [:X,Y:] holds
field W = X \/ Y
let W be Relation; ::_thesis: ( X <> {} & Y <> {} & W = [:X,Y:] implies field W = X \/ Y )
set a = the Element of X;
set b = the Element of Y;
assume that
A1: X <> {} and
A2: Y <> {} and
A3: W = [:X,Y:] ; ::_thesis: field W = X \/ Y
A4: for x being set st x in field W holds
x in X \/ Y
proof
let x be set ; ::_thesis: ( x in field W implies x in X \/ Y )
assume  x in field W ; ::_thesis: x in X \/ Y
then consider y being set  such that
A5: ( [x,y] in W or [y,x] in W ) by Th1;
A6: ( [y,x] in W implies x in X \/ Y )
proof
assume  [y,x] in W ; ::_thesis: x in X \/ Y
then  x in Y by A3, ZFMISC_1:87;
hence  x in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( [x,y] in W implies x in X \/ Y )
proof
assume  [x,y] in W ; ::_thesis: x in X \/ Y
then  x in X by A3, ZFMISC_1:87;
hence  x in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in X \/ Y by A5, A6; ::_thesis: verum
end;
 for x being set st x in X \/ Y holds
x in field W
proof
let x be set ; ::_thesis: ( x in X \/ Y implies x in field W )
A7: ( x in X implies x in field W )
proof
assume  x in X ; ::_thesis: x in field W
then  [x, the Element of Y] in W by A2, A3, ZFMISC_1:87;
hence  x in field W by Th1; ::_thesis: verum
end;
A8: ( x in Y implies x in field W )
proof
assume  x in Y ; ::_thesis: x in field W
then  [ the Element of X,x] in W by A1, A3, ZFMISC_1:87;
hence  x in field W by Th1; ::_thesis: verum
end;
assume  x in X \/ Y ; ::_thesis: x in field W
hence  x in field W by A7, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  field W = X \/ Y by A4, TARSKI:1; ::_thesis: verum
end;

scheme :: WELLSET1:sch 1
RSeparation{ F1() ->  set , P1[ Relation] } :
 ex B being set st
for R being Relation holds
( R in B iff ( R in F1() & P1[R] ) )
proof
defpred S1[ set , set ] means ( $1 = $2 & ex S being Relation st
( S = $2 & P1[S] ) );
A1: for y, t, v being set st S1[y,t] & S1[y,v] holds
t = v ;
consider B being set  such that
A2: for t being set holds
( t in B iff ex y being set st
( y in F1() & S1[y,t] ) ) from TARSKI:sch_1(A1);
take  B ; ::_thesis: for R being Relation holds
( R in B iff ( R in F1() & P1[R] ) )
let R be Relation; ::_thesis: ( R in B iff ( R in F1() & P1[R] ) )
 ( R in B implies ex T being Relation st
( T in F1() & T = R & P1[R] ) )
proof
assume  R in B ; ::_thesis: ex T being Relation st
( T in F1() & T = R & P1[R] )
then consider y being set  such that
A3: y in F1() and
A4: y = R and
A5: ex S being Relation st
( S = R & P1[S] ) by A2;
reconsider y = y as Relation by A4;
take  y ; ::_thesis: ( y in F1() & y = R & P1[R] )
thus  ( y in F1() & y = R & P1[R] ) by A3, A4, A5; ::_thesis: verum
end;
hence  ( R in B implies ( R in F1() & P1[R] ) ) ; ::_thesis: ( R in F1() & P1[R] implies R in B )
thus  ( R in F1() & P1[R] implies R in B ) by A2; ::_thesis: verum
end;

theorem Th3: :: WELLSET1:3
for x, y being set
for W being Relation st x in field W & y in field W & W is well-ordering & not x in W -Seg y holds
[y,x] in W
proof
let x, y be set ; ::_thesis: for W being Relation st x in field W & y in field W & W is well-ordering & not x in W -Seg y holds
[y,x] in W
let W be Relation; ::_thesis: ( x in field W & y in field W & W is well-ordering & not x in W -Seg y implies [y,x] in W )
assume that
A1: x in field W and
A2: y in field W and
A3: W is well-ordering ; ::_thesis: ( x in W -Seg y or [y,x] in W )
 W is connected by A3, WELLORD1:def_4;
then  W is_connected_in field W by RELAT_2:def_14;
then A4: ( not x <> y or [x,y] in W or [y,x] in W ) by A1, A2, RELAT_2:def_6;
 W is reflexive by A3, WELLORD1:def_4;
then A5: W is_reflexive_in field W by RELAT_2:def_9;
assume  not x in W -Seg y ; ::_thesis: [y,x] in W
hence  [y,x] in W by A1, A5, A4, RELAT_2:def_1, WELLORD1:1; ::_thesis: verum
end;

theorem Th4: :: WELLSET1:4
for x, y being set
for W being Relation st x in field W & y in field W & W is well-ordering & x in W -Seg y holds
not [y,x] in W
proof
let x, y be set ; ::_thesis: for W being Relation st x in field W & y in field W & W is well-ordering & x in W -Seg y holds
not [y,x] in W
let W be Relation; ::_thesis: ( x in field W & y in field W & W is well-ordering & x in W -Seg y implies not [y,x] in W )
assume that
A1: ( x in field W & y in field W ) and
A2: W is well-ordering ; ::_thesis: ( not x in W -Seg y or not [y,x] in W )
 W is antisymmetric by A2, WELLORD1:def_4;
then A3: W is_antisymmetric_in field W by RELAT_2:def_12;
assume  x in W -Seg y ; ::_thesis: not [y,x] in W
then A4: ( x <> y & [x,y] in W ) by WELLORD1:1;
assume  [y,x] in W ; ::_thesis: contradiction
hence  contradiction by A1, A3, A4, RELAT_2:def_4; ::_thesis: verum
end;

theorem Th5: :: WELLSET1:5
for F being Function
for D being set st ( for X being set st X in D holds
( not F . X in X & F . X in union D ) ) holds
ex R being Relation st
( field R c= union D & 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 ) ) )
proof
let F be Function; ::_thesis: for D being set st ( for X being set st X in D holds
( not F . X in X & F . X in union D ) ) holds
ex R being Relation st
( field R c= union D & 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 ) ) )
let D be set ; ::_thesis: ( ( for X being set st X in D holds
( not F . X in X & F . X in union D ) ) implies ex R being Relation st
( field R c= union D & 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 ) ) ) )
assume A1: for X being set st X in D holds
( not F . X in X & F . X in union D ) ; ::_thesis: ex R being Relation st
( field R c= union D & 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 ) ) )
defpred S1[ 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):] & S1[W] ) ) from WELLSET1:sch_1();
defpred S2[ set , set ] means  ex W being Relation st
( [$1,$2] in W & W in G );
consider S being Relation such that
A3: for x, y being set holds
( [x,y] in S iff ( x in union D & y in union D & S2[x,y] ) ) from RELAT_1:sch_1();
take R = S; ::_thesis: ( field R c= union D & 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 ) ) )
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: ( x in field R implies ( x in union D & ex W being Relation st
( x in field W & W in G ) ) )
assume  x in field R ; ::_thesis: ( x in union D & ex W being Relation st
( x in field W & W in G ) )
then consider y being set  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: ex W being Relation st
( x in field W & W in G )
take  S ; ::_thesis: ( x in field S & S in G )
thus  ( x in field S & S in G ) by A6, Th1; ::_thesis: verum
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: ( 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 ) ) )
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: ( 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 ) ) implies ( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) ) )
assume that
A8: W1 in G and
A9: W2 in G ; ::_thesis: ( ( 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 ) ) )
A10: W2 is well-ordering by A2, A9;
defpred S3[ 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 & S3[x] ) ) from XBOOLE_0: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: ( x in C implies W1 -Seg x = W2 -Seg x )
assume A14: x in C ; ::_thesis: W1 -Seg x = W2 -Seg x
 for y being set holds
( y in W1 -Seg x iff y in W2 -Seg x )
proof
let y be set ; ::_thesis: ( y in W1 -Seg x iff y in W2 -Seg x )
 ( 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: verum
end;
hence  W1 -Seg x = W2 -Seg x by TARSKI:1; ::_thesis: verum
end;
A15: for x being set st x in C holds
W1 -Seg x c= C
proof
let x be set ; ::_thesis: ( x in C implies W1 -Seg x c= C )
assume A16: x in C ; ::_thesis: W1 -Seg x c= C
 for y being set st y in W1 -Seg x holds
y in C
proof
let y be set ; ::_thesis: ( y in W1 -Seg x implies y in C )
assume A17: y in W1 -Seg x ; ::_thesis: y in C
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: verum
end;
hence  W1 -Seg x c= C by TARSKI:def_3; ::_thesis: verum
end;
A25: 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: ( y1 in field W1 & not y1 in C implies ex y3 being set st
( y3 in field W1 & C = W1 -Seg y3 & not y3 in C ) )
set Y = (field W1) \ C;
assume  ( y1 in field W1 & not y1 in C ) ; ::_thesis: ex y3 being set st
( y3 in field W1 & C = W1 -Seg y3 & not y3 in C )
then  (field W1) \ C <> {} by XBOOLE_0:def_5;
then consider a being set  such that
A26: a in (field W1) \ C and
A27: for b being set st b in (field W1) \ C holds
[a,b] in W1 by A12, WELLORD1:6;
take y3 = a; ::_thesis: ( y3 in field W1 & C = W1 -Seg y3 & not y3 in C )
 for x being set holds
( x in C iff x in W1 -Seg y3 )
proof
let x be set ; ::_thesis: ( x in C iff x in W1 -Seg y3 )
thus  ( x in C implies x in W1 -Seg y3 ) ::_thesis: ( x in W1 -Seg y3 implies x in C )
proof
assume that
A28: x in C and
A29: not x in W1 -Seg y3 ; ::_thesis: contradiction
 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 )
proof
assume  y3 <> x ; ::_thesis: y3 in C
then  y3 in W1 -Seg x by A30, WELLORD1:1;
hence  y3 in C by A31; ::_thesis: verum
end;
hence  contradiction by A26, A28, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  ( x in W1 -Seg y3 implies x in C ) ::_thesis: verum
proof
assume that
A32: x in W1 -Seg y3 and
A33: not x in C ; ::_thesis: contradiction
 [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: verum
end;
end;
hence  ( y3 in field W1 & C = W1 -Seg y3 & not y3 in C ) by A26, TARSKI:1, XBOOLE_0:def_5; ::_thesis: verum
end;
A35: for x being set st x in C holds
W2 -Seg x c= C
proof
let x be set ; ::_thesis: ( x in C implies W2 -Seg x c= C )
assume A36: x in C ; ::_thesis: W2 -Seg x c= C
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in W2 -Seg x or y in C )
assume A37: y in W2 -Seg x ; ::_thesis: y in C
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: verum
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: ( y1 in field W2 & not y1 in C implies ex y3 being set st
( y3 in field W2 & C = W2 -Seg y3 & not y3 in C ) )
set Y = (field W2) \ C;
assume  ( y1 in field W2 & not y1 in C ) ; ::_thesis: ex y3 being set st
( y3 in field W2 & C = W2 -Seg y3 & not y3 in C )
then  (field W2) \ C <> {} by XBOOLE_0:def_5;
then consider a being set  such that
A46: a in (field W2) \ C and
A47: for b being set st b in (field W2) \ C holds
[a,b] in W2 by A10, WELLORD1:6;
take y3 = a; ::_thesis: ( y3 in field W2 & C = W2 -Seg y3 & not y3 in C )
 for x being set holds
( x in C iff x in W2 -Seg y3 )
proof
let x be set ; ::_thesis: ( x in C iff x in W2 -Seg y3 )
thus  ( x in C implies x in W2 -Seg y3 ) ::_thesis: ( x in W2 -Seg y3 implies x in C )
proof
assume that
A48: x in C and
A49: not x in W2 -Seg y3 ; ::_thesis: contradiction
 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 )
proof
assume  y3 <> x ; ::_thesis: y3 in C
then  y3 in W2 -Seg x by A50, WELLORD1:1;
hence  y3 in C by A51; ::_thesis: verum
end;
hence  contradiction by A46, A48, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  ( x in W2 -Seg y3 implies x in C ) ::_thesis: verum
proof
assume that
A52: x in W2 -Seg y3 and
A53: not x in C ; ::_thesis: contradiction
 [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: verum
end;
end;
hence  ( y3 in field W2 & C = W2 -Seg y3 & not y3 in C ) by A46, TARSKI:1, XBOOLE_0:def_5; ::_thesis: verum
end;
A55: ( C = field W1 or C = field W2 )
proof
assume  not C = field W1 ; ::_thesis: C = field W2
then  ex x being set st
( ( x in C & not x in field W1 ) or ( x in field W1 & not x in C ) ) by TARSKI:1;
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: contradiction
then  ex x being set st
( ( x in C & not x in field W2 ) or ( x in field W2 & not x in C ) ) by TARSKI:1;
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 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 |_2 (W1 -Seg y3) iff z in W2 |_2 (W2 -Seg y3) )
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: ( z in W2 & z in [:(W2 -Seg y3),(W2 -Seg y3):] )
consider z1, z2 being set  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: verum
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: ( z in W1 & z in [:(W1 -Seg y3),(W1 -Seg y3):] )
consider z1, z2 being set  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: verum
end;
hence  ( z in W1 |_2 (W1 -Seg y3) iff z in W2 |_2 (W2 -Seg y3) ) by A62, XBOOLE_0:def_4; ::_thesis: verum
end;
then  W1 |_2 (W1 -Seg y3) = W2 |_2 (W2 -Seg y3) by TARSKI:1;
hence  contradiction by A11, A56, A58, A59, A61; ::_thesis: verum
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: ( W2 c= W1 & ( for x being set st x in field W2 holds
W2 -Seg x = W1 -Seg x ) )
 for z1, z2 being set st [z1,z2] in W2 holds
[z1,z2] in W1
proof
let z1, z2 be set ; ::_thesis: ( [z1,z2] in W2 implies [z1,z2] in W1 )
assume A77: [z1,z2] in W2 ; ::_thesis: [z1,z2] in W1
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: verum
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: verum
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: ( W1 c= W2 & ( for x being set st x in field W1 holds
W1 -Seg x = W2 -Seg x ) )
 for z1, z2 being set st [z1,z2] in W1 holds
[z1,z2] in W2
proof
let z1, z2 be set ; ::_thesis: ( [z1,z2] in W1 implies [z1,z2] in W2 )
assume A81: [z1,z2] in W1 ; ::_thesis: [z1,z2] in W2
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: verum
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: verum
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: verum
end;
A84: 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: ( x in field R & y in field R & [x,y] in R & [y,x] in R implies x = y )
assume that
 x in field R and
 y in field R and
A85: [x,y] in R and
A86: [y,x] in R ; ::_thesis: x = y
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 by WELLORD1:def_5;
assume A93: W2 c= W1 ; ::_thesis: x = y
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: verum
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 by WELLORD1:def_5;
assume A95: W1 c= W2 ; ::_thesis: x = y
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: verum
end;
hence  x = y by A7, A88, A90, A91; ::_thesis: verum
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: ( W in G implies field W c= field R )
assume A98: W in G ; ::_thesis: field W c= field R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field W or x in field R )
assume  x in field W ; ::_thesis: x in field R
then consider y being set  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: [y,x] in R
 W in bool [:(union D),(union D):] by A2, A98;
then  ex z1, z2 being set 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: verum
end;
 ( [x,y] in W implies [x,y] in R )
proof
assume A102: [x,y] in W ; ::_thesis: [x,y] in R
 W in bool [:(union D),(union D):] by A2, A98;
then  ex z1, z2 being set 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: verum
end;
hence  x in field R by A99, A100, Th1; ::_thesis: verum
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: ( y in field R implies ( R -Seg y in D & F . (R -Seg y) = y ) )
assume A104: y in field R ; ::_thesis: ( R -Seg y in D & F . (R -Seg y) = y )
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 set st x in W -Seg y holds
x in R -Seg y
proof
let x be set ; ::_thesis: ( x in W -Seg y implies x in R -Seg y )
assume A110: x in W -Seg y ; ::_thesis: x in R -Seg y
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: verum
end;
 for x being set st x in R -Seg y holds
x in W -Seg y
proof
let x be set ; ::_thesis: ( x in R -Seg y implies x in W -Seg y )
assume A113: x in R -Seg y ; ::_thesis: x in W -Seg y
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: verum
end;
then  W -Seg y = R -Seg y by A109, TARSKI:1;
hence  ( R -Seg y in D & F . (R -Seg y) = y ) by A2, A105, A106; ::_thesis: verum
end;
A117: 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: ( x in field R & y in field R & x <> y & not [x,y] in R implies [y,x] in R )
assume that
A118: x in field R and
A119: y in field R and
A120: x <> y ; ::_thesis: ( [x,y] in R or [y,x] in R )
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 by WELLORD1:def_5;
assume  W2 c= W1 ; ::_thesis: ( [x,y] in R or [y,x] in R )
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: verum
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 by WELLORD1:def_5;
assume  W1 c= W2 ; ::_thesis: ( [x,y] in R or [y,x] in R )
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: verum
end;
hence  ( [x,y] in R or [y,x] in R ) by A7, A124, A122, A126; ::_thesis: verum
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: ( not Y c= field R or Y = {} or ex b1 being set st
( b1 in Y & R -Seg b1 misses Y ) )
assume that
A131: Y c= field R and
A132: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & R -Seg b1 misses Y )
set y = the Element of Y;
 the Element of Y in field R by A131, A132, TARSKI:def_3;
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 by WELLORD1:def_5;
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 set  such that
A137: a in Y /\ (field W) and
A138: W -Seg a misses Y /\ (field W) by A135, A136, WELLORD1:def_3;
 ex b being set st
( b in Y & R -Seg b misses Y )
proof
take b = a; ::_thesis: ( b in Y & R -Seg b misses Y )
thus  b in Y by A137, XBOOLE_0:def_4; ::_thesis: R -Seg b misses Y
assume  not R -Seg b misses Y ; ::_thesis: contradiction
then consider x being set  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: verum
end;
hence  ex b1 being set st
( b1 in Y & R -Seg b1 misses Y ) ; ::_thesis: verum
end;
A145: 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: ( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R implies [x,z] in R )
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: [x,z] in R
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: ( [x,y] in W & [y,z] in W & W in G )
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 by WELLORD1:def_5;
 W is well-ordering by A2, A152;
then  W well_orders field W by WELLORD1:4;
then A156: W is_reflexive_in field W by WELLORD1:def_5;
A157: ( x in field W1 & y in field W1 ) by A149, RELAT_1:15;
assume  not x in W1 -Seg y ; ::_thesis: [x,y] in W
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: verum
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: verum
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 by WELLORD1:def_5;
 ( 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: verum
end;
then A164: R is_transitive_in field R by RELAT_2:def_8;
A165: for x being set st x in field R holds
[x,x] in R
proof
let x be set ; ::_thesis: ( x in field R implies [x,x] in R )
assume A166: x in field R ; ::_thesis: [x,x] in R
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 by WELLORD1:def_5;
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: verum
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: field W1 = (field R) \/ {(F . (field R))}
A175: field W3 = {}
proof
set z3 = the Element of field W3;
assume  field W3 <> {} ; ::_thesis: contradiction
then  ex z2 being set 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: verum
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: verum
end;
A176: ( field R <> {} implies field W1 = (field R) \/ {(F . (field R))} )
proof
assume  field R <> {} ; ::_thesis: field W1 = (field R) \/ {(F . (field R))}
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: verum
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: ( not x in field W1 or x in field R or x = F . (field R) )
assume  x in field W1 ; ::_thesis: ( x in field R or x = F . (field R) )
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: verum
end;
A179: 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 or [x,y] in W3 or [x,y] in W4 ) )
 ( [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: verum
end;
 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: ( x in field W1 & y in field W1 & x <> y & not [x,y] in W1 implies [y,x] in W1 )
assume that
A180: x in field W1 and
A181: y in field W1 and
A182: x <> y ; ::_thesis: ( [x,y] in W1 or [y,x] in W1 )
A183: ( x in field R or [x,y] in W1 or [y,x] in W1 )
proof
assume  not x in field R ; ::_thesis: ( [x,y] in W1 or [y,x] in W1 )
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: ( [x,y] in W1 or [y,x] in W1 )
then  [y,x] in W3 by A184, ZFMISC_1:106;
hence  ( [x,y] in W1 or [y,x] in W1 ) by A179; ::_thesis: verum
end;
 ( not y = F . (field R) or [x,y] in W1 or [y,x] in W1 )
proof
assume  y = F . (field R) ; ::_thesis: ( [x,y] in W1 or [y,x] in W1 )
then  [x,y] in W4 by A184, TARSKI:def_1;
hence  ( [x,y] in W1 or [y,x] in W1 ) by A179; ::_thesis: verum
end;
hence  ( [x,y] in W1 or [y,x] in W1 ) by A178, A181, A185; ::_thesis: verum
end;
A186: ( y in field R or [x,y] in W1 or [y,x] in W1 )
proof
assume  not y in field R ; ::_thesis: ( [x,y] in W1 or [y,x] in W1 )
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: ( [y,x] in W1 or [x,y] in W1 )
then  [x,y] in W3 by A187, ZFMISC_1:106;
hence  ( [y,x] in W1 or [x,y] in W1 ) by A179; ::_thesis: verum
end;
 ( not x = F . (field R) or [y,x] in W1 or [x,y] in W1 )
proof
assume  x = F . (field R) ; ::_thesis: ( [y,x] in W1 or [x,y] in W1 )
then  [y,x] in W4 by A187, TARSKI:def_1;
hence  ( [y,x] in W1 or [x,y] in W1 ) by A179; ::_thesis: verum
end;
hence  ( [x,y] in W1 or [y,x] in W1 ) by A178, A180, A188; ::_thesis: verum
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: ( [x,y] in W1 or [y,x] in W1 )
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: verum
end;
hence  ( [x,y] in W1 or [y,x] in W1 ) by A183, A186; ::_thesis: verum
end;
then A189: W1 is_connected_in field W1 by RELAT_2:def_6;
assume A190: field R in D ; ::_thesis: contradiction
 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: ( [x,y] in W1 implies [x,y] in [:(union D),(union D):] )
assume A191: [x,y] in W1 ; ::_thesis: [x,y] in [:(union D),(union D):]
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: verum
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 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: ( [x,y] in W1 & y in field R implies ( [x,y] in R & x in field R ) )
assume that
A196: [x,y] in W1 and
A197: y in field R ; ::_thesis: ( [x,y] in R & x in field R )
A198: not [x,y] in W4
proof
assume  [x,y] in W4 ; ::_thesis: contradiction
then  [x,y] = [(F . (field R)),(F . (field R))] by TARSKI:def_1;
hence  contradiction by A194, A197, XTUPLE_0:1; ::_thesis: verum
end;
 not [x,y] in W3 by A194, A197, ZFMISC_1:106;
hence  [x,y] in R by A179, A196, A198; ::_thesis: x in field R
 ( [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: verum
end;
 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: ( x in field W1 & y in field W1 & [x,y] in W1 & [y,x] in W1 implies x = y )
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: x = y
A203: ( x in field R implies x = y )
proof
assume A204: x in field R ; ::_thesis: x = y
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: verum
end;
A207: ( y in field R implies x = y )
proof
assume A208: y in field R ; ::_thesis: x = y
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: verum
end;
 ( y in field R or y = F . (field R) ) by A178, A200;
hence  x = y by A178, A199, A203, A207; ::_thesis: verum
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: ( y in field R implies W1 -Seg y = R -Seg y )
assume A213: y in field R ; ::_thesis: W1 -Seg y = R -Seg y
A214: for x being set st x in W1 -Seg y holds
x in R -Seg y
proof
let x be set ; ::_thesis: ( x in W1 -Seg y implies x in R -Seg y )
assume A215: x in W1 -Seg y ; ::_thesis: x in R -Seg y
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: verum
end;
 for x being set st x in R -Seg y holds
x in W1 -Seg y
proof
let x be set ; ::_thesis: ( x in R -Seg y implies x in W1 -Seg y )
assume A217: x in R -Seg y ; ::_thesis: x in W1 -Seg y
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: verum
end;
hence  W1 -Seg y = R -Seg y by A214, TARSKI:1; ::_thesis: verum
end;
A219: W1 is_well_founded_in field W1
proof
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= field W1 or Y = {} or ex b1 being set st
( b1 in Y & W1 -Seg b1 misses Y ) )
assume that
A220: Y c= field W1 and
A221: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & W1 -Seg b1 misses Y )
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: ex a being set st
( a in Y & W1 -Seg a misses Y )
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: ex a being set st
( a in Y & W1 -Seg a misses Y )
then consider y being set  such that
A225: y in (field R) /\ Y and
A226: R -Seg y misses (field R) /\ Y by A130, A224, WELLORD1:def_3;
A227: (R -Seg y) /\ Y c= (R -Seg y) /\ ((field R) /\ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R -Seg y) /\ Y or x in (R -Seg y) /\ ((field R) /\ Y) )
assume A228: x in (R -Seg y) /\ Y ; ::_thesis: x in (R -Seg y) /\ ((field R) /\ Y)
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: verum
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: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not z in W1 -Seg (F . (field R)) or z in field R )
assume A233: z in W1 -Seg (F . (field R)) ; ::_thesis: z in field R
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: verum
end;
A235: the Element of Y in field W1 by A220, A221, TARSKI:def_3;
assume A236: (field R) /\ Y = {} ; ::_thesis: ex a being set st
( a in Y & W1 -Seg a misses Y )
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: verum
end;
hence  ex a being set st
( a in Y & W1 -Seg a misses Y ) by A223; ::_thesis: verum
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: ex a being set st
( a in Y & W1 -Seg a misses Y )
then consider b being set  such that
A238: ( b in Y & R -Seg b misses Y ) by A130, A221, WELLORD1:def_3;
take  b ; ::_thesis: ( b in Y & W1 -Seg b misses Y )
thus  ( b in Y & W1 -Seg b misses Y ) by A212, A237, A238; ::_thesis: verum
end;
hence  ex b1 being set st
( b1 in Y & W1 -Seg b1 misses Y ) by A222; ::_thesis: verum
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: ( y in field W1 implies ( W1 -Seg y in D & F . (W1 -Seg y) = y ) )
A240: ( y in field R implies W1 -Seg y = R -Seg y )
proof
assume A241: y in field R ; ::_thesis: W1 -Seg y = R -Seg y
A242: for x being set st x in W1 -Seg y holds
x in R -Seg y
proof
let x be set ; ::_thesis: ( x in W1 -Seg y implies x in R -Seg y )
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: x in R -Seg y
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: verum
end;
 for x being set st x in R -Seg y holds
x in W1 -Seg y
proof
let x be set ; ::_thesis: ( x in R -Seg y implies x in W1 -Seg y )
assume A246: x in R -Seg y ; ::_thesis: x in W1 -Seg y
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: verum
end;
hence  W1 -Seg y = R -Seg y by A242, TARSKI:1; ::_thesis: verum
end;
A248: for x being set st x in W1 -Seg (F . (field R)) holds
x in field R
proof
let x be set ; ::_thesis: ( x in W1 -Seg (F . (field R)) implies x in field R )
assume A249: x in W1 -Seg (F . (field R)) ; ::_thesis: x in field R
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: verum
end;
A251: for x being set st x in field R holds
x in W1 -Seg (F . (field R))
proof
let x be set ; ::_thesis: ( x in field R implies x in W1 -Seg (F . (field R)) )
assume A252: x in field R ; ::_thesis: x in W1 -Seg (F . (field R))
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: verum
end;
assume  y in field W1 ; ::_thesis: ( W1 -Seg y in D & F . (W1 -Seg y) = y )
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:1; ::_thesis: verum
end;
 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: ( x in field W1 & y in field W1 & z in field W1 & [x,y] in W1 & [y,z] in W1 implies [x,z] in W1 )
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: [x,z] in W1
A257: ( z = F . (field R) implies [x,z] in W1 )
proof
assume A258: z = F . (field R) ; ::_thesis: [x,z] in W1
A259: ( x = F . (field R) implies [x,z] in W1 )
proof
assume  x = F . (field R) ; ::_thesis: [x,z] in W1
then  [x,z] in W4 by A258, TARSKI:def_1;
hence  [x,z] in W1 by A179; ::_thesis: verum
end;
 ( x in field R implies [x,z] in W1 )
proof
assume  x in field R ; ::_thesis: [x,z] in W1
then  [x,z] in W3 by A258, ZFMISC_1:106;
hence  [x,z] in W1 by A179; ::_thesis: verum
end;
hence  [x,z] in W1 by A178, A253, A259; ::_thesis: verum
end;
 ( z in field R implies [x,z] in W1 )
proof
assume A260: z in field R ; ::_thesis: [x,z] in W1
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: verum
end;
hence  [x,z] in W1 by A178, A254, A257; ::_thesis: verum
end;
then A263: W1 is_transitive_in field W1 by RELAT_2:def_8;
 for x being set st x in field W1 holds
[x,x] in W1
proof
let x be set ; ::_thesis: ( x in field W1 implies [x,x] in W1 )
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: [x,x] in W1
hence  [x,x] in W1 by A179, A265; ::_thesis: verum
end;
A266: ( x in field R implies [x,x] in W1 )
proof
assume  x in field R ; ::_thesis: [x,x] in W1
then  [x,x] in R by A165;
hence  [x,x] in W1 by A179; ::_thesis: verum
end;
assume  x in field W1 ; ::_thesis: [x,x] in W1
hence  [x,x] in W1 by A178, A266, A264; ::_thesis: verum
end;
then  W1 is_reflexive_in field W1 by RELAT_2:def_1;
then  W1 well_orders field W1 by A263, A211, A189, A219, WELLORD1:def_5;
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: verum
end;
 R is_reflexive_in field R by A165, RELAT_2:def_1;
then  R well_orders field R by A164, A96, A129, A130, WELLORD1:def_5;
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: verum
end;

Lm1:  for X, M being set holds
( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
proof
let X, M be set ; ::_thesis: ( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
A1: ( ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) implies X,M are_equipotent )
proof
assume  ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; ::_thesis: X,M are_equipotent
hence  ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: according to TARSKI:def_6 ::_thesis: verum
end;
 ( X,M are_equipotent implies ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
proof
assume  ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: according to TARSKI:def_6 ::_thesis: ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) )
hence  ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; ::_thesis: verum
end;
hence  ( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ) by A1; ::_thesis: verum
end;

theorem :: WELLSET1:6
for N being set ex R being Relation st
( R is well-ordering & field R = N )
proof
let N be set ; ::_thesis: ex R being Relation st
( R is well-ordering & field R = N )
consider M being set  such that
A1: ( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) ) and
A2: for X being set st X in M holds
bool X in M and
A3: for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by ZFMISC_1:112;
defpred S1[ set ] means  not $1,M are_equipotent ;
consider D being set  such that
A4: for A being set holds
( A in D iff ( A in bool M & S1[A] ) ) from XBOOLE_0:sch_1();
A5: union D c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union D or x in M )
assume  x in union D ; ::_thesis: x in M
then consider A being set  such that
A6: x in A and
A7: A in D by TARSKI:def_4;
 A in bool M by A4, A7;
hence  x in M by A6; ::_thesis: verum
end;
set F = id D;
 for Z being set st Z in D holds
( not (id D) . Z in Z & (id D) . Z in union D )
proof
let Z be set ; ::_thesis: ( Z in D implies ( not (id D) . Z in Z & (id D) . Z in union D ) )
assume A8: Z in D ; ::_thesis: ( not (id D) . Z in Z & (id D) . Z in union D )
 not Z in Z ;
hence  not (id D) . Z in Z by A8, FUNCT_1:18; ::_thesis: (id D) . Z in union D
 for X being set st X in D holds
X in union D
proof
let X be set ; ::_thesis: ( X in D implies X in union D )
A9: X in {X} by TARSKI:def_1;
assume  X in D ; ::_thesis: X in union D
then A10: ( X in bool M & not X,M are_equipotent ) by A4;
A11: not {X},M are_equipotent
proof
A12: X <> bool X
proof
assume  X = bool X ; ::_thesis: contradiction
then  not X in bool X ;
hence  contradiction by ZFMISC_1:def_1; ::_thesis: verum
end;
assume  {X},M are_equipotent ; ::_thesis: contradiction
then consider Z being set  such that
 for x being set st x in {X} holds
ex y being set st
( y in M & [x,y] in Z ) and
A13: for y being set st y in M holds
ex x being set st
( x in {X} & [x,y] in Z ) and
A14: for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) by Lm1;
 bool X in M by A2, A3, A10;
then consider y being set  such that
A15: y in {X} and
A16: [y,(bool X)] in Z by A13;
consider x being set  such that
A17: x in {X} and
A18: [x,X] in Z by A3, A10, A13;
 x = X by A17, TARSKI:def_1;
then  y = x by A15, TARSKI:def_1;
hence  contradiction by A14, A12, A18, A16; ::_thesis: verum
end;
 X in M by A3, A10;
then  for x being set st x in {X} holds
x in M by TARSKI:def_1;
then  {X} c= M by TARSKI:def_3;
then  {X} in D by A4, A11;
hence  X in union D by A9, TARSKI:def_4; ::_thesis: verum
end;
then  Z in union D by A8;
hence  (id D) . Z in union D by A8, FUNCT_1:18; ::_thesis: verum
end;
then consider S being Relation such that
A19: field S c= union D and
A20: S is well-ordering and
A21: not field S in D and
 for y being set st y in field S holds
( S -Seg y in D & (id D) . (S -Seg y) = y ) by Th5;
 ( not field S c= M or field S,M are_equipotent ) by A4, A21;
then consider Z being set  such that
A22: for x being set st x in field S holds
ex y being set st
( y in M & [x,y] in Z ) and
A23: for y being set st y in M holds
ex x being set st
( x in field S & [x,y] in Z ) and
A24: for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) by A5, A19, Lm1, XBOOLE_1:1;
defpred S2[ set , set ] means [$2,$1] in Z;
A25: for x being set st x in M holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in M implies ex y being set st S2[x,y] )
assume  x in M ; ::_thesis: ex y being set st S2[x,y]
then  ex y being set st
( y in field S & [y,x] in Z ) by A23;
hence  ex y being set st S2[x,y] ; ::_thesis: verum
end;
A26: for x, z1, z2 being set st x in M & S2[x,z1] & S2[x,z2] holds
z1 = z2 by A24;
consider H being Function such that
A27: dom H = M and
A28: for x being set st x in M holds
S2[x,H . x] from FUNCT_1:sch_2(A26, A25);
defpred S3[ set , set ] means $2 = {$1};
defpred S4[ set ] means  ex x, y being set st
( $1 = [x,y] & [(H . x),(H . y)] in S );
consider W0 being set  such that
A29: for z being set holds
( z in W0 iff ( z in [:M,M:] & S4[z] ) ) from XBOOLE_0:sch_1();
A30: for x being set st x in field S holds
x in rng H
proof
let x be set ; ::_thesis: ( x in field S implies x in rng H )
assume  x in field S ; ::_thesis: x in rng H
then consider y being set  such that
A31: y in M and
A32: [x,y] in Z by A22;
set z1 = H . y;
 ( H . y in rng H & [(H . y),y] in Z ) by A27, A28, A31, FUNCT_1:def_3;
hence  x in rng H by A24, A32; ::_thesis: verum
end;
 for z1, z2 being set st z1 in dom H & z2 in dom H & H . z1 = H . z2 holds
z1 = z2
proof
let z1, z2 be set ; ::_thesis: ( z1 in dom H & z2 in dom H & H . z1 = H . z2 implies z1 = z2 )
assume that
A33: ( z1 in dom H & z2 in dom H ) and
A34: H . z1 = H . z2 ; ::_thesis: z1 = z2
 ( [(H . z1),z1] in Z & [(H . z2),z2] in Z ) by A27, A28, A33;
hence  z1 = z2 by A24, A34; ::_thesis: verum
end;
then A35: H is one-to-one by FUNCT_1:def_4;
 for z being set st z in W0 holds
ex x, y being set st z = [x,y]
proof
let z be set ; ::_thesis: ( z in W0 implies ex x, y being set st z = [x,y] )
assume  z in W0 ; ::_thesis: ex x, y being set st z = [x,y]
then  ex z1, z2 being set st
( z = [z1,z2] & [(H . z1),(H . z2)] in S ) by A29;
hence  ex x, y being set st z = [x,y] ; ::_thesis: verum
end;
then reconsider W0 = W0 as Relation by RELAT_1:def_1;
A36: for z being set st z in field W0 holds
z in M
proof
let z be set ; ::_thesis: ( z in field W0 implies z in M )
assume  z in field W0 ; ::_thesis: z in M
then consider z1 being set  such that
A37: ( [z,z1] in W0 or [z1,z] in W0 ) by Th1;
A38: ( [z1,z] in W0 implies z in M )
proof
assume  [z1,z] in W0 ; ::_thesis: z in M
then  [z1,z] in [:M,M:] by A29;
hence  z in M by ZFMISC_1:87; ::_thesis: verum
end;
 ( [z,z1] in W0 implies z in M )
proof
assume  [z,z1] in W0 ; ::_thesis: z in M
then  [z,z1] in [:M,M:] by A29;
hence  z in M by ZFMISC_1:87; ::_thesis: verum
end;
hence  z in M by A37, A38; ::_thesis: verum
end;
A39: for x being set st x in N holds
ex y being set st S3[x,y] ;
A40: for x, z1, z2 being set st x in N & S3[x,z1] & S3[x,z2] holds
z1 = z2 ;
consider H1 being Function such that
A41: dom H1 = N and
A42: for x being set st x in N holds
S3[x,H1 . x] from FUNCT_1:sch_2(A40, A39);
 for z1, z2 being set st z1 in dom H1 & z2 in dom H1 & H1 . z1 = H1 . z2 holds
z1 = z2
proof
let z1, z2 be set ; ::_thesis: ( z1 in dom H1 & z2 in dom H1 & H1 . z1 = H1 . z2 implies z1 = z2 )
assume that
A43: z1 in dom H1 and
A44: z2 in dom H1 and
A45: H1 . z1 = H1 . z2 ; ::_thesis: z1 = z2
 H1 . z1 = {z1} by A41, A42, A43;
then A46: z1 in H1 . z2 by A45, TARSKI:def_1;
 H1 . z2 = {z2} by A41, A42, A44;
hence  z1 = z2 by A46, TARSKI:def_1; ::_thesis: verum
end;
then A47: H1 is one-to-one by FUNCT_1:def_4;
set S1 = W0 |_2 (rng H1);
 for x being set st x in rng H holds
x in field S
proof
let x be set ; ::_thesis: ( x in rng H implies x in field S )
assume  x in rng H ; ::_thesis: x in field S
then consider z1 being set  such that
A48: ( z1 in dom H & x = H . z1 ) by FUNCT_1:def_3;
 ( ex z2 being set st
( z2 in field S & [z2,z1] in Z ) & [x,z1] in Z ) by A23, A27, A28, A48;
hence  x in field S by A24; ::_thesis: verum
end;
then A49: rng H = field S by A30, TARSKI:1;
 for z being set st z in M holds
z in field W0
proof
let z be set ; ::_thesis: ( z in M implies z in field W0 )
assume A50: z in M ; ::_thesis: z in field W0
 ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 )
proof
 H . z in field S by A27, A49, A50, FUNCT_1:def_3;
then consider z2 being set  such that
A51: ( [(H . z),z2] in S or [z2,(H . z)] in S ) by Th1;
A52: ( [(H . z),z2] in S implies ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 ) )
proof
assume A53: [(H . z),z2] in S ; ::_thesis: ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 )
then  z2 in rng H by A49, RELAT_1:15;
then consider z3 being set  such that
A54: z3 in dom H and
A55: z2 = H . z3 by FUNCT_1:def_3;
take  z3 ; ::_thesis: ( [z,z3] in W0 or [z3,z] in W0 )
 [z,z3] in [:M,M:] by A27, A50, A54, ZFMISC_1:87;
hence  ( [z,z3] in W0 or [z3,z] in W0 ) by A29, A53, A55; ::_thesis: verum
end;
 ( [z2,(H . z)] in S implies ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 ) )
proof
assume A56: [z2,(H . z)] in S ; ::_thesis: ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 )
then  z2 in rng H by A49, RELAT_1:15;
then consider z3 being set  such that
A57: z3 in dom H and
A58: z2 = H . z3 by FUNCT_1:def_3;
take  z3 ; ::_thesis: ( [z,z3] in W0 or [z3,z] in W0 )
 [z3,z] in [:M,M:] by A27, A50, A57, ZFMISC_1:87;
hence  ( [z,z3] in W0 or [z3,z] in W0 ) by A29, A56, A58; ::_thesis: verum
end;
hence  ex z1 being set st
( [z,z1] in W0 or [z1,z] in W0 ) by A51, A52; ::_thesis: verum
end;
hence  z in field W0 by Th1; ::_thesis: verum
end;
then A59: field W0 = M by A36, TARSKI:1;
 for a, b being set holds
( [a,b] in W0 iff ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) )
proof
let a, b be set ; ::_thesis: ( [a,b] in W0 iff ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) )
A60: ( [a,b] in W0 implies ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) )
proof
assume A61: [a,b] in W0 ; ::_thesis: ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S )
then A62: [a,b] in [:M,M:] by A29;
consider x, y being set  such that
A63: [a,b] = [x,y] and
A64: [(H . x),(H . y)] in S by A29, A61;
 a = x by A63, XTUPLE_0:1;
hence  ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) by A59, A62, A63, A64, XTUPLE_0:1, ZFMISC_1:87; ::_thesis: verum
end;
 ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S implies [a,b] in W0 )
proof
assume that
A65: ( a in field W0 & b in field W0 ) and
A66: [(H . a),(H . b)] in S ; ::_thesis: [a,b] in W0
 [a,b] in [:M,M:] by A59, A65, ZFMISC_1:87;
hence  [a,b] in W0 by A29, A66; ::_thesis: verum
end;
hence  ( [a,b] in W0 iff ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) ) by A60; ::_thesis: verum
end;
then  H is_isomorphism_of W0,S by A27, A35, A49, A59, WELLORD1:def_7;
then A67: H " is_isomorphism_of S,W0 by WELLORD1:39;
then  W0 is well-ordering by A20, WELLORD1:44;
then A68: W0 |_2 (rng H1) is well-ordering by WELLORD1:25;
defpred S5[ set ] means  ex x, y being set st
( $1 = [x,y] & [(H1 . x),(H1 . y)] in W0 |_2 (rng H1) );
consider W00 being set  such that
A69: for z being set holds
( z in W00 iff ( z in [:N,N:] & S5[z] ) ) from XBOOLE_0:sch_1();
 for z being set st z in W00 holds
ex x, y being set st z = [x,y]
proof
let z be set ; ::_thesis: ( z in W00 implies ex x, y being set st z = [x,y] )
assume  z in W00 ; ::_thesis: ex x, y being set st z = [x,y]
then  ex z1, z2 being set st
( z = [z1,z2] & [(H1 . z1),(H1 . z2)] in W0 |_2 (rng H1) ) by A69;
hence  ex x, y being set st z = [x,y] ; ::_thesis: verum
end;
then reconsider W00 = W00 as Relation by RELAT_1:def_1;
A70: for z being set st z in field W00 holds
z in N
proof
let z be set ; ::_thesis: ( z in field W00 implies z in N )
assume  z in field W00 ; ::_thesis: z in N
then consider z1 being set  such that
A71: ( [z,z1] in W00 or [z1,z] in W00 ) by Th1;
A72: ( [z1,z] in W00 implies z in N )
proof
assume  [z1,z] in W00 ; ::_thesis: z in N
then  [z1,z] in [:N,N:] by A69;
hence  z in N by ZFMISC_1:87; ::_thesis: verum
end;
 ( [z,z1] in W00 implies z in N )
proof
assume  [z,z1] in W00 ; ::_thesis: z in N
then  [z,z1] in [:N,N:] by A69;
hence  z in N by ZFMISC_1:87; ::_thesis: verum
end;
hence  z in N by A71, A72; ::_thesis: verum
end;
 rng H1 c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng H1 or x in M )
assume  x in rng H1 ; ::_thesis: x in M
then consider y being set  such that
A73: y in dom H1 and
A74: x = H1 . y by FUNCT_1:def_3;
 for z1 being set st z1 in {y} holds
z1 in N by A41, A73, TARSKI:def_1;
then A75: {y} c= N by TARSKI:def_3;
 x = {y} by A41, A42, A73, A74;
hence  x in M by A1, A75; ::_thesis: verum
end;
then A76: field (W0 |_2 (rng H1)) = rng H1 by A20, A59, A67, WELLORD1:31, WELLORD1:44;
 for z being set st z in N holds
z in field W00
proof
let z be set ; ::_thesis: ( z in N implies z in field W00 )
assume A77: z in N ; ::_thesis: z in field W00
 ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 )
proof
 H1 . z in field (W0 |_2 (rng H1)) by A41, A76, A77, FUNCT_1:def_3;
then consider z2 being set  such that
A78: ( [(H1 . z),z2] in W0 |_2 (rng H1) or [z2,(H1 . z)] in W0 |_2 (rng H1) ) by Th1;
A79: ( [(H1 . z),z2] in W0 |_2 (rng H1) implies ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 ) )
proof
assume A80: [(H1 . z),z2] in W0 |_2 (rng H1) ; ::_thesis: ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 )
then  z2 in rng H1 by A76, RELAT_1:15;
then consider z3 being set  such that
A81: z3 in dom H1 and
A82: z2 = H1 . z3 by FUNCT_1:def_3;
take  z3 ; ::_thesis: ( [z,z3] in W00 or [z3,z] in W00 )
 [z,z3] in [:N,N:] by A41, A77, A81, ZFMISC_1:87;
hence  ( [z,z3] in W00 or [z3,z] in W00 ) by A69, A80, A82; ::_thesis: verum
end;
 ( [z2,(H1 . z)] in W0 |_2 (rng H1) implies ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 ) )
proof
assume A83: [z2,(H1 . z)] in W0 |_2 (rng H1) ; ::_thesis: ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 )
then  z2 in rng H1 by A76, RELAT_1:15;
then consider z3 being set  such that
A84: z3 in dom H1 and
A85: z2 = H1 . z3 by FUNCT_1:def_3;
take  z3 ; ::_thesis: ( [z,z3] in W00 or [z3,z] in W00 )
 [z3,z] in [:N,N:] by A41, A77, A84, ZFMISC_1:87;
hence  ( [z,z3] in W00 or [z3,z] in W00 ) by A69, A83, A85; ::_thesis: verum
end;
hence  ex z1 being set st
( [z,z1] in W00 or [z1,z] in W00 ) by A78, A79; ::_thesis: verum
end;
hence  z in field W00 by Th1; ::_thesis: verum
end;
then A86: field W00 = N by A70, TARSKI:1;
 for a, b being set holds
( [a,b] in W00 iff ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) )
proof
let a, b be set ; ::_thesis: ( [a,b] in W00 iff ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) )
A87: ( [a,b] in W00 implies ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) )
proof
assume A88: [a,b] in W00 ; ::_thesis: ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) )
then A89: [a,b] in [:N,N:] by A69;
consider x, y being set  such that
A90: [a,b] = [x,y] and
A91: [(H1 . x),(H1 . y)] in W0 |_2 (rng H1) by A69, A88;
 a = x by A90, XTUPLE_0:1;
hence  ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) by A86, A89, A90, A91, XTUPLE_0:1, ZFMISC_1:87; ::_thesis: verum
end;
 ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) implies [a,b] in W00 )
proof
assume that
A92: ( a in field W00 & b in field W00 ) and
A93: [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ; ::_thesis: [a,b] in W00
 [a,b] in [:N,N:] by A86, A92, ZFMISC_1:87;
hence  [a,b] in W00 by A69, A93; ::_thesis: verum
end;
hence  ( [a,b] in W00 iff ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) ) by A87; ::_thesis: verum
end;
then  H1 is_isomorphism_of W00,W0 |_2 (rng H1) by A41, A47, A76, A86, WELLORD1:def_7;
then  H1 " is_isomorphism_of W0 |_2 (rng H1),W00 by WELLORD1:39;
hence  ex R being Relation st
( R is well-ordering & field R = N ) by A68, A86, WELLORD1:44; ::_thesis: verum
end;