:: WELLORD1 semantic presentation

begin

             Lm1:  for R being Relation holds
( R is reflexive iff for x being set st x in field R holds
[x,x] in R )
proof
let R be Relation; ::_thesis: ( R is reflexive iff for x being set st x in field R holds
[x,x] in R )
 ( R is reflexive iff R is_reflexive_in field R ) by RELAT_2:def_9;
hence  ( R is reflexive iff for x being set st x in field R holds
[x,x] in R ) by RELAT_2:def_1; ::_thesis: verum
end;

Lm2:  for R being Relation holds
( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
proof
let R be Relation; ::_thesis: ( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
thus  ( R is transitive implies for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ) ::_thesis: ( ( for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ) implies R is transitive )
proof
assume  R is transitive ; ::_thesis: for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R
then A1: R is_transitive_in field R by RELAT_2:def_16;
let x, y, z be set ; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A2: [x,y] in R and
A3: [y,z] in R ; ::_thesis: [x,z] in R
A4: z in field R by A3, RELAT_1:15;
 ( x in field R & y in field R ) by A2, RELAT_1:15;
hence  [x,z] in R by A1, A2, A3, A4, RELAT_2:def_8; ::_thesis: verum
end;
assume  for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ; ::_thesis: R is transitive
then  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 ;
then  R is_transitive_in field R by RELAT_2:def_8;
hence  R is transitive by RELAT_2:def_16; ::_thesis: verum
end;

Lm3:  for R being Relation holds
( R is antisymmetric iff for x, y being set st [x,y] in R & [y,x] in R holds
x = y )
proof
let R be Relation; ::_thesis: ( R is antisymmetric iff for x, y being set st [x,y] in R & [y,x] in R holds
x = y )
thus  ( R is antisymmetric implies for x, y being set st [x,y] in R & [y,x] in R holds
x = y ) ::_thesis: ( ( for x, y being set st [x,y] in R & [y,x] in R holds
x = y ) implies R is antisymmetric )
proof
assume  R is antisymmetric ; ::_thesis: for x, y being set st [x,y] in R & [y,x] in R holds
x = y
then A1: R is_antisymmetric_in field R by RELAT_2:def_12;
let x, y be set ; ::_thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume that
A2: [x,y] in R and
A3: [y,x] in R ; ::_thesis: x = y
 ( x in field R & y in field R ) by A2, RELAT_1:15;
hence  x = y by A1, A2, A3, RELAT_2:def_4; ::_thesis: verum
end;
assume  for x, y being set st [x,y] in R & [y,x] in R holds
x = y ; ::_thesis: R is antisymmetric
then  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 ;
then  R is_antisymmetric_in field R by RELAT_2:def_4;
hence  R is antisymmetric by RELAT_2:def_12; ::_thesis: verum
end;

Lm4:  for R being Relation holds
( R is connected iff 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 R be Relation; ::_thesis: ( R is connected iff 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 )
 ( R is connected iff R is_connected_in field R ) by RELAT_2:def_14;
hence  ( R is connected iff 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 ) by RELAT_2:def_6; ::_thesis: verum
end;

definition
let R be Relation;
let a be set ;
funcR -Seg a ->  set  equals :: WELLORD1:def 1
(Coim (R,a)) \ {a};
coherence
 (Coim (R,a)) \ {a} is set ;
end;

:: deftheorem  defines -Seg WELLORD1:def_1_:_
 for R being Relation
for a being set holds R -Seg a = (Coim (R,a)) \ {a};

theorem Th1: :: WELLORD1:1
for x, a being set
for R being Relation holds
( x in R -Seg a iff ( x <> a & [x,a] in R ) )
proof
let x, a be set ; ::_thesis: for R being Relation holds
( x in R -Seg a iff ( x <> a & [x,a] in R ) )
let R be Relation; ::_thesis: ( x in R -Seg a iff ( x <> a & [x,a] in R ) )
hereby  ::_thesis: ( x <> a & [x,a] in R implies x in R -Seg a )
assume A1: x in R -Seg a ; ::_thesis: ( x <> a & [x,a] in R )
hence  x <> a by ZFMISC_1:56; ::_thesis: [x,a] in R
 ex y being set st
( [x,y] in R & y in {a} ) by A1, RELAT_1:def_14;
hence  [x,a] in R by TARSKI:def_1; ::_thesis: verum
end;
assume that
A2: x <> a and
A3: [x,a] in R ; ::_thesis: x in R -Seg a
 a in {a} by TARSKI:def_1;
then  x in Coim (R,a) by A3, RELAT_1:def_14;
hence  x in R -Seg a by A2, ZFMISC_1:56; ::_thesis: verum
end;

theorem Th2: :: WELLORD1:2
for x being set
for R being Relation holds
( x in field R or R -Seg x = {} )
proof
let x be set ; ::_thesis: for R being Relation holds
( x in field R or R -Seg x = {} )
let R be Relation; ::_thesis: ( x in field R or R -Seg x = {} )
assume A1: not x in field R ; ::_thesis: R -Seg x = {}
set y = the Element of R -Seg x;
assume  R -Seg x <> {} ; ::_thesis: contradiction
then  [ the Element of R -Seg x,x] in R by Th1;
hence  contradiction by A1, RELAT_1:15; ::_thesis: verum
end;

definition
let R be Relation;
attrR is well_founded  means :Def2: :: WELLORD1:def 2
 for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y );
let X be set ;
predR is_well_founded_in X means :Def3: :: WELLORD1:def 3
 for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y );
end;

:: deftheorem Def2 defines well_founded WELLORD1:def_2_:_
 for R being Relation holds
( R is well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) );

:: deftheorem Def3 defines is_well_founded_in WELLORD1:def_3_:_
 for R being Relation
for X being set holds
( R is_well_founded_in X iff for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) );

theorem Th3: :: WELLORD1:3
for R being Relation holds
( R is well_founded iff R is_well_founded_in field R )
proof
let R be Relation; ::_thesis: ( R is well_founded iff R is_well_founded_in field R )
thus  ( R is well_founded implies R is_well_founded_in field R ) ::_thesis: ( R is_well_founded_in field R implies R is well_founded )
proof
assume  for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def_2 ::_thesis: R is_well_founded_in field R
hence  for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def_3 ::_thesis: verum
end;
assume  for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def_3 ::_thesis: R is well_founded
hence  for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def_2 ::_thesis: verum
end;

definition
let R be Relation;
attrR is well-ordering  means :Def4: :: WELLORD1:def 4
( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded );
let X be set ;
predR well_orders X means :Def5: :: WELLORD1:def 5
( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X );
end;

:: deftheorem Def4 defines well-ordering WELLORD1:def_4_:_
 for R being Relation holds
( R is well-ordering iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) );

:: deftheorem Def5 defines well_orders WELLORD1:def_5_:_
 for R being Relation
for X being set holds
( R well_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) );

registration
cluster Relation-like well-ordering  ->  reflexive antisymmetric connected transitive well_founded for set ;
coherence
 for b1 being Relation st b1 is well-ordering holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) by Def4;
cluster Relation-like reflexive antisymmetric connected transitive well_founded  ->  well-ordering for set ;
coherence
 for b1 being Relation st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded holds
b1 is well-ordering by Def4;
end;

theorem :: WELLORD1:4
for R being Relation holds
( R well_orders field R iff R is well-ordering )
proof
let R be Relation; ::_thesis: ( R well_orders field R iff R is well-ordering )
thus  ( R well_orders field R implies R is well-ordering ) ::_thesis: ( R is well-ordering implies R well_orders field R )
proof
assume  ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in field R ) ; :: according to WELLORD1:def_5 ::_thesis: R is well-ordering
hence  ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) by Th3, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_14, RELAT_2:def_16; :: according to WELLORD1:def_4 ::_thesis: verum
end;
assume  ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) ; :: according to WELLORD1:def_4 ::_thesis: R well_orders field R
hence  ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in field R ) by Th3, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_14, RELAT_2:def_16; :: according to WELLORD1:def_5 ::_thesis: verum
end;

theorem :: WELLORD1:5
for X being set
for R being Relation st R well_orders X holds
for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
proof
let X be set ; ::_thesis: for R being Relation st R well_orders X holds
for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
let R be Relation; ::_thesis: ( R well_orders X implies for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume A1: R well_orders X ; ::_thesis: for Y being set st Y c= X & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
then A2: R is_reflexive_in X by Def5;
A3: R is_connected_in X by A1, Def5;
let Y be set ; ::_thesis: ( Y c= X & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume that
A4: Y c= X and
A5: Y <> {} ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
 R is_well_founded_in X by A1, Def5;
then consider a being set  such that
A6: a in Y and
A7: R -Seg a misses Y by A4, A5, Def3;
take  a ; ::_thesis: ( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
thus  a in Y by A6; ::_thesis: for b being set st b in Y holds
[a,b] in R
let b be set ; ::_thesis: ( b in Y implies [a,b] in R )
assume A8: b in Y ; ::_thesis: [a,b] in R
then  not b in R -Seg a by A7, XBOOLE_0:3;
then  ( a = b or not [b,a] in R ) by Th1;
then  ( a <> b implies [a,b] in R ) by A3, A4, A6, A8, RELAT_2:def_6;
hence  [a,b] in R by A2, A4, A6, RELAT_2:def_1; ::_thesis: verum
end;

theorem Th6: :: WELLORD1:6
for R being Relation st R is well-ordering holds
for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
proof
let R be Relation; ::_thesis: ( R is well-ordering implies for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume A1: R is well-ordering ; ::_thesis: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
let Y be set ; ::_thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) ) )
assume that
A2: Y c= field R and
A3: Y <> {} ; ::_thesis: ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
consider a being set  such that
A4: a in Y and
A5: R -Seg a misses Y by A1, A2, A3, Def2;
take  a ; ::_thesis: ( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )
thus  a in Y by A4; ::_thesis: for b being set st b in Y holds
[a,b] in R
let b be set ; ::_thesis: ( b in Y implies [a,b] in R )
assume A6: b in Y ; ::_thesis: [a,b] in R
then  not b in R -Seg a by A5, XBOOLE_0:3;
then  ( a = b or not [b,a] in R ) by Th1;
then  ( a <> b implies [a,b] in R ) by A1, A2, A4, A6, Lm4;
hence  [a,b] in R by A1, A2, A4, Lm1; ::_thesis: verum
end;

theorem :: WELLORD1:7
for R being Relation st R is well-ordering & field R <> {} holds
ex a being set st
( a in field R & ( for b being set st b in field R holds
[a,b] in R ) ) by Th6;

theorem :: WELLORD1:8
for R being Relation st R is well-ordering holds
for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
proof
let R be Relation; ::_thesis: ( R is well-ordering implies for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) ) )
assume A1: R is well-ordering ; ::_thesis: for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
let a be set ; ::_thesis: ( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
assume A2: a in field R ; ::_thesis: ( for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
defpred S1[ set ] means  not [$1,a] in R;
given b being set  such that A3: ( b in field R & not [b,a] in R ) ; ::_thesis: ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) )
consider Z being set  such that
A4: for c being set holds
( c in Z iff ( c in field R & S1[c] ) ) from XBOOLE_0:sch_1();
 for b being set st b in Z holds
b in field R by A4;
then A5: Z c= field R by TARSKI:def_3;
 Z <> {} by A3, A4;
then consider d being set  such that
A6: d in Z and
A7: for c being set st c in Z holds
[d,c] in R by A1, A5, Th6;
take  d ; ::_thesis: ( d in field R & [a,d] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R ) )
thus A8: d in field R by A4, A6; ::_thesis: ( [a,d] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R ) )
A9: not [d,a] in R by A4, A6;
then  a <> d by A6, A7;
hence  [a,d] in R by A1, A2, A8, A9, Lm4; ::_thesis: for c being set st c in field R & [a,c] in R & not c = a holds
[d,c] in R
let c be set ; ::_thesis: ( c in field R & [a,c] in R & not c = a implies [d,c] in R )
assume that
A10: c in field R and
A11: [a,c] in R ; ::_thesis: ( c = a or [d,c] in R )
assume  c <> a ; ::_thesis: [d,c] in R
then  not [c,a] in R by A1, A11, Lm3;
then  c in Z by A4, A10;
hence  [d,c] in R by A7; ::_thesis: verum
end;


theorem Th9: :: WELLORD1:9
for a being set
for R being Relation holds R -Seg a c= field R
proof
let a be set ; ::_thesis: for R being Relation holds R -Seg a c= field R
let R be Relation; ::_thesis: R -Seg a c= field R
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in R -Seg a or b in field R )
assume  b in R -Seg a ; ::_thesis: b in field R
then  [b,a] in R by Th1;
hence  b in field R by RELAT_1:15; ::_thesis: verum
end;

definition
let R be Relation;
let Y be set ;
funcR |_2 Y ->  Relation equals :: WELLORD1:def 6
R /\ [:Y,Y:];
coherence
 R /\ [:Y,Y:] is Relation ;
end;

:: deftheorem  defines |_2 WELLORD1:def_6_:_
 for R being Relation
for Y being set holds R |_2 Y = R /\ [:Y,Y:];

theorem Th10: :: WELLORD1:10
for X being set
for R being Relation holds R |_2 X = (X |` R) | X
proof
let X be set ; ::_thesis: for R being Relation holds R |_2 X = (X |` R) | X
let R be Relation; ::_thesis: R |_2 X = (X |` R) | X
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R |_2 X or [x,b1] in (X |` R) | X ) & ( not [x,b1] in (X |` R) | X or [x,b1] in R |_2 X ) )
let y be set ; ::_thesis: ( ( not [x,y] in R |_2 X or [x,y] in (X |` R) | X ) & ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X ) )
thus  ( [x,y] in R |_2 X implies [x,y] in (X |` R) | X ) ::_thesis: ( not [x,y] in (X |` R) | X or [x,y] in R |_2 X )
proof
assume A1: [x,y] in R |_2 X ; ::_thesis: [x,y] in (X |` R) | X
then A2: [x,y] in [:X,X:] by XBOOLE_0:def_4;
then A3: x in X by ZFMISC_1:87;
A4: y in X by A2, ZFMISC_1:87;
 [x,y] in R by A1, XBOOLE_0:def_4;
then  [x,y] in X |` R by A4, RELAT_1:def_12;
hence  [x,y] in (X |` R) | X by A3, RELAT_1:def_11; ::_thesis: verum
end;
assume A5: [x,y] in (X |` R) | X ; ::_thesis: [x,y] in R |_2 X
then A6: [x,y] in X |` R by RELAT_1:def_11;
then A7: [x,y] in R by RELAT_1:def_12;
A8: y in X by A6, RELAT_1:def_12;
 x in X by A5, RELAT_1:def_11;
then  [x,y] in [:X,X:] by A8, ZFMISC_1:87;
hence  [x,y] in R |_2 X by A7, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th11: :: WELLORD1:11
for X being set
for R being Relation holds R |_2 X = X |` (R | X)
proof
let X be set ; ::_thesis: for R being Relation holds R |_2 X = X |` (R | X)
let R be Relation; ::_thesis: R |_2 X = X |` (R | X)
thus R |_2 X = (X |` R) | X by Th10
.= X |` (R | X) by RELAT_1:109 ; ::_thesis: verum
end;

Lm5:  for X being set
for R being Relation holds dom (X |` R) c= dom R
proof
let X be set ; ::_thesis: for R being Relation holds dom (X |` R) c= dom R
let R be Relation; ::_thesis: dom (X |` R) c= dom R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (X |` R) or x in dom R )
assume  x in dom (X |` R) ; ::_thesis: x in dom R
then consider y being set  such that
A1: [x,y] in X |` R by XTUPLE_0:def_12;
 [x,y] in R by A1, RELAT_1:def_12;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th12: :: WELLORD1:12
for x, X being set
for R being Relation st x in field (R |_2 X) holds
( x in field R & x in X )
proof
let x, X be set ; ::_thesis: for R being Relation st x in field (R |_2 X) holds
( x in field R & x in X )
let R be Relation; ::_thesis: ( x in field (R |_2 X) implies ( x in field R & x in X ) )
A1: ( dom ((X |` R) | X) = (dom (X |` R)) /\ X & rng (X |` (R | X)) = (rng (R | X)) /\ X ) by RELAT_1:61, RELAT_1:88;
assume  x in field (R |_2 X) ; ::_thesis: ( x in field R & x in X )
then A2: ( x in dom (R |_2 X) or x in rng (R |_2 X) ) by XBOOLE_0:def_3;
A3: ( dom (X |` R) c= dom R & rng (R | X) c= rng R ) by Lm5, RELAT_1:70;
 ( R |_2 X = (X |` R) | X & R |_2 X = X |` (R | X) ) by Th10, Th11;
then  ( ( x in dom (X |` R) & x in X ) or ( x in rng (R | X) & x in X ) ) by A2, A1, XBOOLE_0:def_4;
hence  ( x in field R & x in X ) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th13: :: WELLORD1:13
for X being set
for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X )
proof
let X be set ; ::_thesis: for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X )
let R be Relation; ::_thesis: ( field (R |_2 X) c= field R & field (R |_2 X) c= X )
 ( ( for x being set st x in field (R |_2 X) holds
x in field R ) & ( for x being set st x in field (R |_2 X) holds
x in X ) ) by Th12;
hence  ( field (R |_2 X) c= field R & field (R |_2 X) c= X ) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th14: :: WELLORD1:14
for X, a being set
for R being Relation holds (R |_2 X) -Seg a c= R -Seg a
proof
let X, a be set ; ::_thesis: for R being Relation holds (R |_2 X) -Seg a c= R -Seg a
let R be Relation; ::_thesis: (R |_2 X) -Seg a c= R -Seg a
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R |_2 X) -Seg a or x in R -Seg a )
assume A1: x in (R |_2 X) -Seg a ; ::_thesis: x in R -Seg a
then  [x,a] in R |_2 X by Th1;
then A2: [x,a] in R by XBOOLE_0:def_4;
 x <> a by A1, Th1;
hence  x in R -Seg a by A2, Th1; ::_thesis: verum
end;

theorem Th15: :: WELLORD1:15
for X being set
for R being Relation st R is reflexive holds
R |_2 X is reflexive
proof
let X be set ; ::_thesis: for R being Relation st R is reflexive holds
R |_2 X is reflexive
let R be Relation; ::_thesis: ( R is reflexive implies R |_2 X is reflexive )
assume A1: R is reflexive ; ::_thesis: R |_2 X is reflexive
now__::_thesis:_for_a_being_set_st_a_in_field_(R_|_2_X)_holds_
[a,a]_in_R_|_2_X
let a be set ; ::_thesis: ( a in field (R |_2 X) implies [a,a] in R |_2 X )
assume A2: a in field (R |_2 X) ; ::_thesis: [a,a] in R |_2 X
then  a in X by Th12;
then A3: [a,a] in [:X,X:] by ZFMISC_1:87;
 a in field R by A2, Th12;
then  [a,a] in R by A1, Lm1;
hence  [a,a] in R |_2 X by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  R |_2 X is reflexive by Lm1; ::_thesis: verum
end;

theorem Th16: :: WELLORD1:16
for Y being set
for R being Relation st R is connected holds
R |_2 Y is connected
proof
let Y be set ; ::_thesis: for R being Relation st R is connected holds
R |_2 Y is connected
let R be Relation; ::_thesis: ( R is connected implies R |_2 Y is connected )
assume A1: R is connected ; ::_thesis: R |_2 Y is connected
now__::_thesis:_for_a,_b_being_set_st_a_in_field_(R_|_2_Y)_&_b_in_field_(R_|_2_Y)_&_a_<>_b_&_not_[a,b]_in_R_|_2_Y_holds_
[b,a]_in_R_|_2_Y
let a, b be set ; ::_thesis: ( a in field (R |_2 Y) & b in field (R |_2 Y) & a <> b & not [a,b] in R |_2 Y implies [b,a] in R |_2 Y )
assume that
A2: ( a in field (R |_2 Y) & b in field (R |_2 Y) ) and
A3: a <> b ; ::_thesis: ( [a,b] in R |_2 Y or [b,a] in R |_2 Y )
 ( a in Y & b in Y ) by A2, Th12;
then A4: ( [a,b] in [:Y,Y:] & [b,a] in [:Y,Y:] ) by ZFMISC_1:87;
 ( a in field R & b in field R ) by A2, Th12;
then  ( [a,b] in R or [b,a] in R ) by A1, A3, Lm4;
hence  ( [a,b] in R |_2 Y or [b,a] in R |_2 Y ) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  R |_2 Y is connected by Lm4; ::_thesis: verum
end;

theorem Th17: :: WELLORD1:17
for Y being set
for R being Relation st R is transitive holds
R |_2 Y is transitive
proof
let Y be set ; ::_thesis: for R being Relation st R is transitive holds
R |_2 Y is transitive
let R be Relation; ::_thesis: ( R is transitive implies R |_2 Y is transitive )
assume A1: R is transitive ; ::_thesis: R |_2 Y is transitive
now__::_thesis:_for_a,_b,_c_being_set_st_[a,b]_in_R_|_2_Y_&_[b,c]_in_R_|_2_Y_holds_
[a,c]_in_R_|_2_Y
let a, b, c be set ; ::_thesis: ( [a,b] in R |_2 Y & [b,c] in R |_2 Y implies [a,c] in R |_2 Y )
assume that
A2: [a,b] in R |_2 Y and
A3: [b,c] in R |_2 Y ; ::_thesis: [a,c] in R |_2 Y
 ( [a,b] in R & [b,c] in R ) by A2, A3, XBOOLE_0:def_4;
then A4: [a,c] in R by A1, Lm2;
 [b,c] in [:Y,Y:] by A3, XBOOLE_0:def_4;
then A5: c in Y by ZFMISC_1:87;
 [a,b] in [:Y,Y:] by A2, XBOOLE_0:def_4;
then  a in Y by ZFMISC_1:87;
then  [a,c] in [:Y,Y:] by A5, ZFMISC_1:87;
hence  [a,c] in R |_2 Y by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  R |_2 Y is transitive by Lm2; ::_thesis: verum
end;

theorem Th18: :: WELLORD1:18
for Y being set
for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric
proof
let Y be set ; ::_thesis: for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric
let R be Relation; ::_thesis: ( R is antisymmetric implies R |_2 Y is antisymmetric )
assume A1: R is antisymmetric ; ::_thesis: R |_2 Y is antisymmetric
now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_R_|_2_Y_&_[b,a]_in_R_|_2_Y_holds_
a_=_b
let a, b be set ; ::_thesis: ( [a,b] in R |_2 Y & [b,a] in R |_2 Y implies a = b )
assume  ( [a,b] in R |_2 Y & [b,a] in R |_2 Y ) ; ::_thesis: a = b
then  ( [a,b] in R & [b,a] in R ) by XBOOLE_0:def_4;
hence  a = b by A1, Lm3; ::_thesis: verum
end;
hence  R |_2 Y is antisymmetric by Lm3; ::_thesis: verum
end;

theorem Th19: :: WELLORD1:19
for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)
let R be Relation; ::_thesis: (R |_2 X) |_2 Y = R |_2 (X /\ Y)
thus (R |_2 X) |_2 Y = R /\ ([:X,X:] /\ [:Y,Y:]) by XBOOLE_1:16
.= R |_2 (X /\ Y) by ZFMISC_1:100 ; ::_thesis: verum
end;

theorem :: WELLORD1:20
for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
let R be Relation; ::_thesis: (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
thus (R |_2 X) |_2 Y = R |_2 (Y /\ X) by Th19
.= (R |_2 Y) |_2 X by Th19 ; ::_thesis: verum
end;

theorem :: WELLORD1:21
for Y being set
for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y
proof
let Y be set ; ::_thesis: for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y
let R be Relation; ::_thesis: (R |_2 Y) |_2 Y = R |_2 Y
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [a,b1] in (R |_2 Y) |_2 Y or [a,b1] in R |_2 Y ) & ( not [a,b1] in R |_2 Y or [a,b1] in (R |_2 Y) |_2 Y ) )
let b be set ; ::_thesis: ( ( not [a,b] in (R |_2 Y) |_2 Y or [a,b] in R |_2 Y ) & ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y ) )
thus  ( [a,b] in (R |_2 Y) |_2 Y implies [a,b] in R |_2 Y ) by XBOOLE_0:def_4; ::_thesis: ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y )
assume A1: [a,b] in R |_2 Y ; ::_thesis: [a,b] in (R |_2 Y) |_2 Y
then  [a,b] in [:Y,Y:] by XBOOLE_0:def_4;
hence  [a,b] in (R |_2 Y) |_2 Y by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th22: :: WELLORD1:22
for Z, Y being set
for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z
proof
let Z, Y be set ; ::_thesis: for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z
let R be Relation; ::_thesis: ( Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z )
assume A1: Z c= Y ; ::_thesis: (R |_2 Y) |_2 Z = R |_2 Z
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [a,b1] in (R |_2 Y) |_2 Z or [a,b1] in R |_2 Z ) & ( not [a,b1] in R |_2 Z or [a,b1] in (R |_2 Y) |_2 Z ) )
let b be set ; ::_thesis: ( ( not [a,b] in (R |_2 Y) |_2 Z or [a,b] in R |_2 Z ) & ( not [a,b] in R |_2 Z or [a,b] in (R |_2 Y) |_2 Z ) )
thus  ( [a,b] in (R |_2 Y) |_2 Z implies [a,b] in R |_2 Z ) ::_thesis: ( not [a,b] in R |_2 Z or [a,b] in (R |_2 Y) |_2 Z )
proof
assume A2: [a,b] in (R |_2 Y) |_2 Z ; ::_thesis: [a,b] in R |_2 Z
then  [a,b] in R |_2 Y by XBOOLE_0:def_4;
then A3: [a,b] in R by XBOOLE_0:def_4;
 [a,b] in [:Z,Z:] by A2, XBOOLE_0:def_4;
hence  [a,b] in R |_2 Z by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: [a,b] in R |_2 Z ; ::_thesis: [a,b] in (R |_2 Y) |_2 Z
then A5: [a,b] in R by XBOOLE_0:def_4;
A6: [a,b] in [:Z,Z:] by A4, XBOOLE_0:def_4;
then  ( a in Z & b in Z ) by ZFMISC_1:87;
then  [a,b] in [:Y,Y:] by A1, ZFMISC_1:87;
then  [a,b] in R |_2 Y by A5, XBOOLE_0:def_4;
hence  [a,b] in (R |_2 Y) |_2 Z by A6, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th23: :: WELLORD1:23
for R being Relation holds R |_2 (field R) = R
proof
let R be Relation; ::_thesis: R |_2 (field R) = R
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R |_2 (field R) or [x,b1] in R ) & ( not [x,b1] in R or [x,b1] in R |_2 (field R) ) )
let y be set ; ::_thesis: ( ( not [x,y] in R |_2 (field R) or [x,y] in R ) & ( not [x,y] in R or [x,y] in R |_2 (field R) ) )
thus  ( [x,y] in R |_2 (field R) implies [x,y] in R ) by XBOOLE_0:def_4; ::_thesis: ( not [x,y] in R or [x,y] in R |_2 (field R) )
assume A1: [x,y] in R ; ::_thesis: [x,y] in R |_2 (field R)
then  ( x in field R & y in field R ) by RELAT_1:15;
then  [x,y] in [:(field R),(field R):] by ZFMISC_1:87;
hence  [x,y] in R |_2 (field R) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th24: :: WELLORD1:24
for X being set
for R being Relation st R is well_founded holds
R |_2 X is well_founded
proof
let X be set ; ::_thesis: for R being Relation st R is well_founded holds
R |_2 X is well_founded
let R be Relation; ::_thesis: ( R is well_founded implies R |_2 X is well_founded )
assume A1: for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def_2 ::_thesis: R |_2 X is well_founded
A2: field (R |_2 X) c= field R by Th13;
let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( Y c= field (R |_2 X) & Y <> {} implies ex a being set st
( a in Y & (R |_2 X) -Seg a misses Y ) )
assume  ( Y c= field (R |_2 X) & Y <> {} ) ; ::_thesis: ex a being set st
( a in Y & (R |_2 X) -Seg a misses Y )
then consider a being set  such that
A3: a in Y and
A4: R -Seg a misses Y by A1, A2, XBOOLE_1:1;
take  a ; ::_thesis: ( a in Y & (R |_2 X) -Seg a misses Y )
thus  a in Y by A3; ::_thesis: (R |_2 X) -Seg a misses Y
assume  not (R |_2 X) -Seg a misses Y ; ::_thesis: contradiction
then A5: ex b being set st
( b in (R |_2 X) -Seg a & b in Y ) by XBOOLE_0:3;
 (R |_2 X) -Seg a c= R -Seg a by Th14;
hence  contradiction by A4, A5, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th25: :: WELLORD1:25
for Y being set
for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering
proof
let Y be set ; ::_thesis: for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering
let R be Relation; ::_thesis: ( R is well-ordering implies R |_2 Y is well-ordering )
assume  R is well-ordering ; ::_thesis: R |_2 Y is well-ordering
hence  ( R |_2 Y is reflexive & R |_2 Y is transitive & R |_2 Y is antisymmetric & R |_2 Y is connected & R |_2 Y is well_founded ) by Th15, Th16, Th17, Th18, Th24; :: according to WELLORD1:def_4 ::_thesis: verum
end;

theorem Th26: :: WELLORD1:26
for a, b being set
for R being Relation st R is well-ordering holds
R -Seg a,R -Seg b are_c=-comparable
proof
let a, b be set ; ::_thesis: for R being Relation st R is well-ordering holds
R -Seg a,R -Seg b are_c=-comparable
let R be Relation; ::_thesis: ( R is well-ordering implies R -Seg a,R -Seg b are_c=-comparable )
assume A1: R is well-ordering ; ::_thesis: R -Seg a,R -Seg b are_c=-comparable
A2: now__::_thesis:_(_a_in_field_R_&_b_in_field_R_implies_R_-Seg_a,R_-Seg_b_are_c=-comparable_)
assume A3: ( a in field R & b in field R ) ; ::_thesis: R -Seg a,R -Seg b are_c=-comparable
now__::_thesis:_(_a_<>_b_implies_R_-Seg_a,R_-Seg_b_are_c=-comparable_)
assume  a <> b ; ::_thesis: R -Seg a,R -Seg b are_c=-comparable
A4: now__::_thesis:_(_[b,a]_in_R_implies_R_-Seg_b_c=_R_-Seg_a_)
assume A5: [b,a] in R ; ::_thesis: R -Seg b c= R -Seg a
now__::_thesis:_for_c_being_set_st_c_in_R_-Seg_b_holds_
c_in_R_-Seg_a
let c be set ; ::_thesis: ( c in R -Seg b implies c in R -Seg a )
assume A6: c in R -Seg b ; ::_thesis: c in R -Seg a
then A7: [c,b] in R by Th1;
then A8: [c,a] in R by A1, A5, Lm2;
 c <> b by A6, Th1;
then  c <> a by A1, A5, A7, Lm3;
hence  c in R -Seg a by A8, Th1; ::_thesis: verum
end;
hence  R -Seg b c= R -Seg a by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(_[a,b]_in_R_implies_R_-Seg_a_c=_R_-Seg_b_)
assume A9: [a,b] in R ; ::_thesis: R -Seg a c= R -Seg b
now__::_thesis:_for_c_being_set_st_c_in_R_-Seg_a_holds_
c_in_R_-Seg_b
let c be set ; ::_thesis: ( c in R -Seg a implies c in R -Seg b )
assume A10: c in R -Seg a ; ::_thesis: c in R -Seg b
then A11: [c,a] in R by Th1;
then A12: [c,b] in R by A1, A9, Lm2;
 c <> a by A10, Th1;
then  c <> b by A1, A9, A11, Lm3;
hence  c in R -Seg b by A12, Th1; ::_thesis: verum
end;
hence  R -Seg a c= R -Seg b by TARSKI:def_3; ::_thesis: verum
end;
hence  R -Seg a,R -Seg b are_c=-comparable by A1, A3, A4, Lm4, XBOOLE_0:def_9; ::_thesis: verum
end;
hence  R -Seg a,R -Seg b are_c=-comparable ; ::_thesis: verum
end;
now__::_thesis:_(_(_R_-Seg_a_=_{}_or_R_-Seg_b_=_{}_)_implies_R_-Seg_a,R_-Seg_b_are_c=-comparable_)
assume  ( R -Seg a = {} or R -Seg b = {} ) ; ::_thesis: R -Seg a,R -Seg b are_c=-comparable
then  ( R -Seg a c= R -Seg b or R -Seg b c= R -Seg a ) by XBOOLE_1:2;
hence  R -Seg a,R -Seg b are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
hence  R -Seg a,R -Seg b are_c=-comparable by A2, Th2; ::_thesis: verum
end;

theorem Th27: :: WELLORD1:27
for b, a being set
for R being Relation st R is well-ordering & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b
proof
let b, a be set ; ::_thesis: for R being Relation st R is well-ordering & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b
let R be Relation; ::_thesis: ( R is well-ordering & b in R -Seg a implies (R |_2 (R -Seg a)) -Seg b = R -Seg b )
assume that
A1: R is well-ordering and
A2: b in R -Seg a ; ::_thesis: (R |_2 (R -Seg a)) -Seg b = R -Seg b
set S = R |_2 (R -Seg a);
now__::_thesis:_for_c_being_set_st_c_in_R_-Seg_b_holds_
c_in_(R_|_2_(R_-Seg_a))_-Seg_b
let c be set ; ::_thesis: ( c in R -Seg b implies c in (R |_2 (R -Seg a)) -Seg b )
assume A3: c in R -Seg b ; ::_thesis: c in (R |_2 (R -Seg a)) -Seg b
then A4: [c,b] in R by Th1;
A5: [b,a] in R by A2, Th1;
then A6: [c,a] in R by A1, A4, Lm2;
A7: c <> b by A3, Th1;
then  c <> a by A1, A4, A5, Lm3;
then  c in R -Seg a by A6, Th1;
then  [c,b] in [:(R -Seg a),(R -Seg a):] by A2, ZFMISC_1:87;
then  [c,b] in R |_2 (R -Seg a) by A4, XBOOLE_0:def_4;
hence  c in (R |_2 (R -Seg a)) -Seg b by A7, Th1; ::_thesis: verum
end;
then A8: R -Seg b c= (R |_2 (R -Seg a)) -Seg b by TARSKI:def_3;
now__::_thesis:_for_c_being_set_st_c_in_(R_|_2_(R_-Seg_a))_-Seg_b_holds_
c_in_R_-Seg_b
let c be set ; ::_thesis: ( c in (R |_2 (R -Seg a)) -Seg b implies c in R -Seg b )
assume A9: c in (R |_2 (R -Seg a)) -Seg b ; ::_thesis: c in R -Seg b
then  [c,b] in R |_2 (R -Seg a) by Th1;
then A10: [c,b] in R by XBOOLE_0:def_4;
 c <> b by A9, Th1;
hence  c in R -Seg b by A10, Th1; ::_thesis: verum
end;
then  (R |_2 (R -Seg a)) -Seg b c= R -Seg b by TARSKI:def_3;
hence  (R |_2 (R -Seg a)) -Seg b = R -Seg b by A8, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th28: :: WELLORD1:28
for Y being set
for R being Relation st R is well-ordering & Y c= field R holds
( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )
proof
let Y be set ; ::_thesis: for R being Relation st R is well-ordering & Y c= field R holds
( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )
let R be Relation; ::_thesis: ( R is well-ordering & Y c= field R implies ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ) )
assume that
A1: R is well-ordering and
A2: Y c= field R ; ::_thesis: ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )
now__::_thesis:_(_ex_a_being_set_st_
(_a_in_field_R_&_Y_=_R_-Seg_a_)_implies_for_b_being_set_st_b_in_Y_holds_
for_c_being_set_st_[c,b]_in_R_holds_
c_in_Y_)
given a being set  such that  a in field R and
A3: Y = R -Seg a ; ::_thesis: for b being set st b in Y holds
for c being set st [c,b] in R holds
c in Y
let b be set ; ::_thesis: ( b in Y implies for c being set st [c,b] in R holds
c in Y )
assume A4: b in Y ; ::_thesis: for c being set st [c,b] in R holds
c in Y
A5: [b,a] in R by A3, A4, Th1;
let c be set ; ::_thesis: ( [c,b] in R implies c in Y )
assume A6: [c,b] in R ; ::_thesis: c in Y
A7: [c,a] in R by A1, A6, A5, Lm2;
 b <> a by A3, A4, Th1;
then  c <> a by A1, A6, A5, Lm3;
hence  c in Y by A3, A7, Th1; ::_thesis: verum
end;
hence  ( ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) ) implies for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ) by RELAT_1:15; ::_thesis: ( ex a being set st
( a in Y & ex b being set st
( [b,a] in R & not b in Y ) ) or Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) )
assume A8: for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y ; ::_thesis: ( Y = field R or ex a being set st
( a in field R & Y = R -Seg a ) )
assume  Y <> field R ; ::_thesis: ex a being set st
( a in field R & Y = R -Seg a )
then  not for d being set holds
( d in field R iff d in Y ) by TARSKI:1;
then  (field R) \ Y <> {} by A2, XBOOLE_0:def_5;
then consider a being set  such that
A9: a in (field R) \ Y and
A10: for b being set st b in (field R) \ Y holds
[a,b] in R by A1, Th6;
A11: now__::_thesis:_for_b_being_set_st_b_in_R_-Seg_a_holds_
b_in_Y
let b be set ; ::_thesis: ( b in R -Seg a implies b in Y )
assume A12: b in R -Seg a ; ::_thesis: b in Y
then A13: [b,a] in R by Th1;
assume A14: not b in Y ; ::_thesis: contradiction
 b in field R by A13, RELAT_1:15;
then  b in (field R) \ Y by A14, XBOOLE_0:def_5;
then A15: [a,b] in R by A10;
 b <> a by A12, Th1;
hence  contradiction by A1, A13, A15, Lm3; ::_thesis: verum
end;
take  a ; ::_thesis: ( a in field R & Y = R -Seg a )
thus  a in field R by A9; ::_thesis: Y = R -Seg a
now__::_thesis:_for_b_being_set_st_b_in_Y_holds_
b_in_R_-Seg_a
A16: not a in Y by A9, XBOOLE_0:def_5;
let b be set ; ::_thesis: ( b in Y implies b in R -Seg a )
assume A17: b in Y ; ::_thesis: b in R -Seg a
assume  not b in R -Seg a ; ::_thesis: contradiction
then A18: ( not [b,a] in R or a = b ) by Th1;
 a <> b by A9, A17, XBOOLE_0:def_5;
then  [a,b] in R by A2, A1, A9, A17, A18, Lm4;
hence  contradiction by A8, A17, A16; ::_thesis: verum
end;
hence  Y = R -Seg a by A11, TARSKI:1; ::_thesis: verum
end;

theorem Th29: :: WELLORD1:29
for a, b being set
for R being Relation st R is well-ordering & a in field R & b in field R holds
( [a,b] in R iff R -Seg a c= R -Seg b )
proof
let a, b be set ; ::_thesis: for R being Relation st R is well-ordering & a in field R & b in field R holds
( [a,b] in R iff R -Seg a c= R -Seg b )
let R be Relation; ::_thesis: ( R is well-ordering & a in field R & b in field R implies ( [a,b] in R iff R -Seg a c= R -Seg b ) )
assume that
A1: R is well-ordering and
A2: a in field R and
A3: b in field R ; ::_thesis: ( [a,b] in R iff R -Seg a c= R -Seg b )
thus  ( [a,b] in R implies R -Seg a c= R -Seg b ) ::_thesis: ( R -Seg a c= R -Seg b implies [a,b] in R )
proof
assume A4: [a,b] in R ; ::_thesis: R -Seg a c= R -Seg b
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in R -Seg a or c in R -Seg b )
assume A5: c in R -Seg a ; ::_thesis: c in R -Seg b
then A6: [c,a] in R by Th1;
then A7: [c,b] in R by A1, A4, Lm2;
 c <> a by A5, Th1;
then  c <> b by A1, A4, A6, Lm3;
hence  c in R -Seg b by A7, Th1; ::_thesis: verum
end;
assume A8: R -Seg a c= R -Seg b ; ::_thesis: [a,b] in R
now__::_thesis:_(_a_<>_b_implies_[a,b]_in_R_)
assume A9: a <> b ; ::_thesis: [a,b] in R
assume  not [a,b] in R ; ::_thesis: contradiction
then  [b,a] in R by A2, A3, A1, A9, Lm4;
then  b in R -Seg a by A9, Th1;
hence  contradiction by A8, Th1; ::_thesis: verum
end;
hence  [a,b] in R by A1, A2, Lm1; ::_thesis: verum
end;

theorem Th30: :: WELLORD1:30
for a, b being set
for R being Relation st R is well-ordering & a in field R & b in field R holds
( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )
proof
let a, b be set ; ::_thesis: for R being Relation st R is well-ordering & a in field R & b in field R holds
( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )
let R be Relation; ::_thesis: ( R is well-ordering & a in field R & b in field R implies ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) ) )
assume A1: ( R is well-ordering & a in field R & b in field R ) ; ::_thesis: ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )
thus  ( not R -Seg a c= R -Seg b or a = b or a in R -Seg b ) ::_thesis: ( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b )
proof
assume  R -Seg a c= R -Seg b ; ::_thesis: ( a = b or a in R -Seg b )
then  [a,b] in R by A1, Th29;
hence  ( a = b or a in R -Seg b ) by Th1; ::_thesis: verum
end;
now__::_thesis:_(_a_in_R_-Seg_b_implies_R_-Seg_a_c=_R_-Seg_b_)
assume  a in R -Seg b ; ::_thesis: R -Seg a c= R -Seg b
then  [a,b] in R by Th1;
hence  R -Seg a c= R -Seg b by A1, Th29; ::_thesis: verum
end;
hence  ( ( a = b or a in R -Seg b ) implies R -Seg a c= R -Seg b ) ; ::_thesis: verum
end;

theorem Th31: :: WELLORD1:31
for X being set
for R being Relation st R is well-ordering & X c= field R holds
field (R |_2 X) = X
proof
let X be set ; ::_thesis: for R being Relation st R is well-ordering & X c= field R holds
field (R |_2 X) = X
let R be Relation; ::_thesis: ( R is well-ordering & X c= field R implies field (R |_2 X) = X )
assume that
A1: R is well-ordering and
A2: X c= field R ; ::_thesis: field (R |_2 X) = X
thus  field (R |_2 X) c= X by Th13; :: according to XBOOLE_0:def_10 ::_thesis: X c= field (R |_2 X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in field (R |_2 X) )
assume A3: x in X ; ::_thesis: x in field (R |_2 X)
then A4: [x,x] in [:X,X:] by ZFMISC_1:87;
 [x,x] in R by A1, A2, A3, Lm1;
then  [x,x] in R |_2 X by A4, XBOOLE_0:def_4;
hence  x in field (R |_2 X) by RELAT_1:15; ::_thesis: verum
end;

theorem Th32: :: WELLORD1:32
for a being set
for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a
proof
let a be set ; ::_thesis: for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a
let R be Relation; ::_thesis: ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a )
 R -Seg a c= field R by Th9;
hence  ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a ) by Th31; ::_thesis: verum
end;

theorem Th33: :: WELLORD1:33
for R being Relation st R is well-ordering holds
for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z
proof
let R be Relation; ::_thesis: ( R is well-ordering implies for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z )
assume A1: R is well-ordering ; ::_thesis: for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z
let Z be set ; ::_thesis: ( ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) implies field R c= Z )
assume A2: for a being set st a in field R & R -Seg a c= Z holds
a in Z ; ::_thesis: field R c= Z
A3: now__::_thesis:_for_a_being_set_st_a_in_field_R_&_(_for_b_being_set_st_[b,a]_in_R_&_a_<>_b_holds_
b_in_Z_)_holds_
a_in_Z
let a be set ; ::_thesis: ( a in field R & ( for b being set st [b,a] in R & a <> b holds
b in Z ) implies a in Z )
assume that
A4: a in field R and
A5: for b being set st [b,a] in R & a <> b holds
b in Z ; ::_thesis: a in Z
now__::_thesis:_for_b_being_set_st_b_in_R_-Seg_a_holds_
b_in_Z
let b be set ; ::_thesis: ( b in R -Seg a implies b in Z )
assume  b in R -Seg a ; ::_thesis: b in Z
then  ( [b,a] in R & b <> a ) by Th1;
hence  b in Z by A5; ::_thesis: verum
end;
then  R -Seg a c= Z by TARSKI:def_3;
hence  a in Z by A2, A4; ::_thesis: verum
end;
given a being set  such that A6: ( a in field R & not a in Z ) ; :: according to TARSKI:def_3 ::_thesis: contradiction
 (field R) \ Z <> {} by A6, XBOOLE_0:def_5;
then consider a being set  such that
A7: a in (field R) \ Z and
A8: for b being set st b in (field R) \ Z holds
[a,b] in R by A1, Th6;
 not a in Z by A7, XBOOLE_0:def_5;
then consider b being set  such that
A9: [b,a] in R and
A10: b <> a and
A11: not b in Z by A3, A7;
 b in field R by A9, RELAT_1:15;
then  b in (field R) \ Z by A11, XBOOLE_0:def_5;
then  [a,b] in R by A8;
hence  contradiction by A1, A9, A10, Lm3; ::_thesis: verum
end;

theorem Th34: :: WELLORD1:34
for a, b being set
for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) holds
[a,b] in R
proof
let a, b be set ; ::_thesis: for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) holds
[a,b] in R
let R be Relation; ::_thesis: ( R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) implies [a,b] in R )
assume that
A1: ( R is well-ordering & a in field R & b in field R ) and
A2: for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ; ::_thesis: [a,b] in R
assume A3: not [a,b] in R ; ::_thesis: contradiction
 a <> b by A1, A3, Lm1;
then  [b,a] in R by A1, A3, Lm4;
then  b in R -Seg a by A3, Th1;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th35: :: WELLORD1:35
for R being Relation
for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being set st a in field R holds
[a,(F . a)] in R
proof
let R be Relation; ::_thesis: for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being set st a in field R holds
[a,(F . a)] in R
let F be Function; ::_thesis: ( R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) implies for a being set st a in field R holds
[a,(F . a)] in R )
assume that
A1: ( R is well-ordering & dom F = field R & rng F c= field R ) and
A2: for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ; ::_thesis: for a being set st a in field R holds
[a,(F . a)] in R
defpred S1[ set ] means [$1,(F . $1)] in R;
consider Z being set  such that
A3: for a being set holds
( a in Z iff ( a in field R & S1[a] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_for_a_being_set_st_a_in_field_R_&_R_-Seg_a_c=_Z_holds_
a_in_Z
let a be set ; ::_thesis: ( a in field R & R -Seg a c= Z implies a in Z )
assume A4: a in field R ; ::_thesis: ( R -Seg a c= Z implies a in Z )
assume A5: R -Seg a c= Z ; ::_thesis: a in Z
A6: now__::_thesis:_for_b_being_set_st_b_in_R_-Seg_a_holds_
(_[b,(F_._a)]_in_R_&_b_<>_F_._a_)
let b be set ; ::_thesis: ( b in R -Seg a implies ( [b,(F . a)] in R & b <> F . a ) )
assume A7: b in R -Seg a ; ::_thesis: ( [b,(F . a)] in R & b <> F . a )
then A8: [b,(F . b)] in R by A3, A5;
A9: ( [b,a] in R & b <> a ) by A7, Th1;
then A10: [(F . b),(F . a)] in R by A2;
hence  [b,(F . a)] in R by A1, A8, Lm2; ::_thesis: b <> F . a
 F . b <> F . a by A2, A9;
hence  b <> F . a by A1, A8, A10, Lm3; ::_thesis: verum
end;
 F . a in rng F by A1, A4, FUNCT_1:def_3;
then  [a,(F . a)] in R by A1, A4, A6, Th34;
hence  a in Z by A3, A4; ::_thesis: verum
end;
then A11: field R c= Z by A1, Th33;
let a be set ; ::_thesis: ( a in field R implies [a,(F . a)] in R )
assume  a in field R ; ::_thesis: [a,(F . a)] in R
hence  [a,(F . a)] in R by A3, A11; ::_thesis: verum
end;

definition
let R, S be Relation;
let F be Function;
predF is_isomorphism_of R,S means :Def7: :: WELLORD1:def 7
( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) );
end;

:: deftheorem Def7 defines is_isomorphism_of WELLORD1:def_7_:_
 for R, S being Relation
for F being Function holds
( F is_isomorphism_of R,S iff ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) );

theorem Th36: :: WELLORD1:36
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )
proof
let R, S be Relation; ::_thesis: for F being Function st F is_isomorphism_of R,S holds
for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )
let F be Function; ::_thesis: ( F is_isomorphism_of R,S implies for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b ) )
assume A1: F is_isomorphism_of R,S ; ::_thesis: for a, b being set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )
then A2: ( dom F = field R & F is one-to-one ) by Def7;
let a, b be set ; ::_thesis: ( [a,b] in R & a <> b implies ( [(F . a),(F . b)] in S & F . a <> F . b ) )
assume that
A3: [a,b] in R and
A4: a <> b ; ::_thesis: ( [(F . a),(F . b)] in S & F . a <> F . b )
 ( a in field R & b in field R ) by A1, A3, Def7;
hence  ( [(F . a),(F . b)] in S & F . a <> F . b ) by A1, A2, A3, A4, Def7, FUNCT_1:def_4; ::_thesis: verum
end;

definition
let R, S be Relation;
predR,S are_isomorphic  means :Def8: :: WELLORD1:def 8
 ex F being Function st F is_isomorphism_of R,S;
end;

:: deftheorem Def8 defines are_isomorphic WELLORD1:def_8_:_
 for R, S being Relation holds
( R,S are_isomorphic iff ex F being Function st F is_isomorphism_of R,S );

theorem Th37: :: WELLORD1:37
for R being Relation holds id (field R) is_isomorphism_of R,R
proof
let R be Relation; ::_thesis: id (field R) is_isomorphism_of R,R
A1: now__::_thesis:_for_a,_b_being_set_holds_
(_(_[a,b]_in_R_implies_(_a_in_field_R_&_b_in_field_R_&_[((id_(field_R))_._a),((id_(field_R))_._b)]_in_R_)_)_&_(_a_in_field_R_&_b_in_field_R_&_[((id_(field_R))_._a),((id_(field_R))_._b)]_in_R_implies_[a,b]_in_R_)_)
let a, b be set ; ::_thesis: ( ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) & ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R ) )
thus  ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) ::_thesis: ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R )
proof
assume A2: [a,b] in R ; ::_thesis: ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R )
hence A3: ( a in field R & b in field R ) by RELAT_1:15; ::_thesis: [((id (field R)) . a),((id (field R)) . b)] in R
then  (id (field R)) . a = a by FUNCT_1:18;
hence  [((id (field R)) . a),((id (field R)) . b)] in R by A2, A3, FUNCT_1:18; ::_thesis: verum
end;
assume that
A4: a in field R and
A5: ( b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ; ::_thesis: [a,b] in R
 (id (field R)) . a = a by A4, FUNCT_1:18;
hence  [a,b] in R by A5, FUNCT_1:18; ::_thesis: verum
end;
 ( dom (id (field R)) = field R & rng (id (field R)) = field R ) ;
hence  id (field R) is_isomorphism_of R,R by A1, Def7; ::_thesis: verum
end;

theorem :: WELLORD1:38
for R being Relation holds R,R are_isomorphic
proof
let R be Relation; ::_thesis: R,R are_isomorphic
take  id (field R) ; :: according to WELLORD1:def_8 ::_thesis: id (field R) is_isomorphism_of R,R
thus  id (field R) is_isomorphism_of R,R by Th37; ::_thesis: verum
end;

theorem Th39: :: WELLORD1:39
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
F " is_isomorphism_of S,R
proof
let R, S be Relation; ::_thesis: for F being Function st F is_isomorphism_of R,S holds
F " is_isomorphism_of S,R
let F be Function; ::_thesis: ( F is_isomorphism_of R,S implies F " is_isomorphism_of S,R )
assume A1: F is_isomorphism_of R,S ; ::_thesis: F " is_isomorphism_of S,R
then A2: F is one-to-one by Def7;
A3: rng F = field S by A1, Def7;
hence A4: dom (F ") = field S by A2, FUNCT_1:33; :: according to WELLORD1:def_7 ::_thesis: ( rng (F ") = field R & F " is one-to-one & ( for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) ) ) )
A5: dom F = field R by A1, Def7;
hence  rng (F ") = field R by A2, FUNCT_1:33; ::_thesis: ( F " is one-to-one & ( for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) ) ) )
thus  F " is one-to-one by A2; ::_thesis: for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) )
let a, b be set ; ::_thesis: ( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) )
thus  ( [a,b] in S implies ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) ) ::_thesis: ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R implies [a,b] in S )
proof
A6: dom F = rng (F ") by A2, FUNCT_1:33;
assume A7: [a,b] in S ; ::_thesis: ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R )
hence A8: ( a in field S & b in field S ) by RELAT_1:15; ::_thesis: [((F ") . a),((F ") . b)] in R
then A9: ( (F ") . a in rng (F ") & (F ") . b in rng (F ") ) by A4, FUNCT_1:def_3;
 ( a = F . ((F ") . a) & b = F . ((F ") . b) ) by A3, A2, A8, FUNCT_1:35;
hence  [((F ") . a),((F ") . b)] in R by A1, A5, A7, A6, A9, Def7; ::_thesis: verum
end;
assume that
A10: ( a in field S & b in field S ) and
A11: [((F ") . a),((F ") . b)] in R ; ::_thesis: [a,b] in S
 ( F . ((F ") . a) = a & F . ((F ") . b) = b ) by A3, A2, A10, FUNCT_1:35;
hence  [a,b] in S by A1, A11, Def7; ::_thesis: verum
end;

theorem Th40: :: WELLORD1:40
for R, S being Relation st R,S are_isomorphic holds
S,R are_isomorphic
proof
let R, S be Relation; ::_thesis: ( R,S are_isomorphic implies S,R are_isomorphic )
given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def_8 ::_thesis: S,R are_isomorphic
take  F " ; :: according to WELLORD1:def_8 ::_thesis: F " is_isomorphism_of S,R
thus  F " is_isomorphism_of S,R by A1, Th39; ::_thesis: verum
end;

theorem Th41: :: WELLORD1:41
for R, S, T being Relation
for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of S,T holds
G * F is_isomorphism_of R,T
proof
let R, S, T be Relation; ::_thesis: for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of S,T holds
G * F is_isomorphism_of R,T
let F, G be Function; ::_thesis: ( F is_isomorphism_of R,S & G is_isomorphism_of S,T implies G * F is_isomorphism_of R,T )
assume that
A1: dom F = field R and
A2: rng F = field S and
A3: F is one-to-one and
A4: for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ; :: according to WELLORD1:def_7 ::_thesis: ( not G is_isomorphism_of S,T or G * F is_isomorphism_of R,T )
assume that
A5: dom G = field S and
A6: rng G = field T and
A7: G is one-to-one and
A8: for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [(G . a),(G . b)] in T ) ) ; :: according to WELLORD1:def_7 ::_thesis: G * F is_isomorphism_of R,T
thus  dom (G * F) = field R by A1, A2, A5, RELAT_1:27; :: according to WELLORD1:def_7 ::_thesis: ( rng (G * F) = field T & G * F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) ) )
thus  rng (G * F) = field T by A2, A5, A6, RELAT_1:28; ::_thesis: ( G * F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) ) )
thus  G * F is one-to-one by A3, A7; ::_thesis: for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) )
let a, b be set ; ::_thesis: ( [a,b] in R iff ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) )
thus  ( [a,b] in R implies ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T ) ) ::_thesis: ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T implies [a,b] in R )
proof
assume A9: [a,b] in R ; ::_thesis: ( a in field R & b in field R & [((G * F) . a),((G * F) . b)] in T )
hence  ( a in field R & b in field R ) by RELAT_1:15; ::_thesis: [((G * F) . a),((G * F) . b)] in T
then A10: ( (G * F) . a = G . (F . a) & (G * F) . b = G . (F . b) ) by A1, FUNCT_1:13;
 [(F . a),(F . b)] in S by A4, A9;
hence  [((G * F) . a),((G * F) . b)] in T by A8, A10; ::_thesis: verum
end;
assume that
A11: ( a in field R & b in field R ) and
A12: [((G * F) . a),((G * F) . b)] in T ; ::_thesis: [a,b] in R
A13: ( (G * F) . a = G . (F . a) & (G * F) . b = G . (F . b) ) by A1, A11, FUNCT_1:13;
 ( F . a in field S & F . b in field S ) by A1, A2, A11, FUNCT_1:def_3;
then  [(F . a),(F . b)] in S by A8, A12, A13;
hence  [a,b] in R by A4, A11; ::_thesis: verum
end;

theorem Th42: :: WELLORD1:42
for R, S, T being Relation st R,S are_isomorphic & S,T are_isomorphic holds
R,T are_isomorphic
proof
let R, S, T be Relation; ::_thesis: ( R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic )
given F being Function such that A1: F is_isomorphism_of R,S ; :: according to WELLORD1:def_8 ::_thesis: ( not S,T are_isomorphic or R,T are_isomorphic )
given G being Function such that A2: G is_isomorphism_of S,T ; :: according to WELLORD1:def_8 ::_thesis: R,T are_isomorphic
take  G * F ; :: according to WELLORD1:def_8 ::_thesis: G * F is_isomorphism_of R,T
thus  G * F is_isomorphism_of R,T by A1, A2, Th41; ::_thesis: verum
end;

theorem Th43: :: WELLORD1:43
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
let R, S be Relation; ::_thesis: for F being Function st F is_isomorphism_of R,S holds
( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
let F be Function; ::_thesis: ( F is_isomorphism_of R,S implies ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) ) )
assume A1: F is_isomorphism_of R,S ; ::_thesis: ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
then A2: dom F = field R by Def7;
A3: rng F = field S by A1, Def7;
A4: F is one-to-one by A1, Def7;
then A5: ( rng (F ") = dom F & dom (F ") = rng F ) by FUNCT_1:33;
thus  ( R is reflexive implies S is reflexive ) ::_thesis: ( ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A6: R is reflexive ; ::_thesis: S is reflexive
now__::_thesis:_for_a_being_set_st_a_in_field_S_holds_
[a,a]_in_S
let a be set ; ::_thesis: ( a in field S implies [a,a] in S )
assume A7: a in field S ; ::_thesis: [a,a] in S
then  (F ") . a in field R by A2, A3, A5, FUNCT_1:def_3;
then A8: [((F ") . a),((F ") . a)] in R by A6, Lm1;
 a = F . ((F ") . a) by A3, A4, A7, FUNCT_1:35;
hence  [a,a] in S by A1, A8, Def7; ::_thesis: verum
end;
hence  S is reflexive by Lm1; ::_thesis: verum
end;
thus  ( R is transitive implies S is transitive ) ::_thesis: ( ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A9: R is transitive ; ::_thesis: S is transitive
now__::_thesis:_for_a,_b,_c_being_set_st_[a,b]_in_S_&_[b,c]_in_S_holds_
[a,c]_in_S
let a, b, c be set ; ::_thesis: ( [a,b] in S & [b,c] in S implies [a,c] in S )
assume that
A10: [a,b] in S and
A11: [b,c] in S ; ::_thesis: [a,c] in S
A12: c in field S by A11, RELAT_1:15;
then A13: c = F . ((F ") . c) by A3, A4, FUNCT_1:35;
 b in field S by A10, RELAT_1:15;
then A14: ( b = F . ((F ") . b) & (F ") . b in field R ) by A2, A3, A4, A5, FUNCT_1:35, FUNCT_1:def_3;
 (F ") . c in field R by A2, A3, A5, A12, FUNCT_1:def_3;
then A15: [((F ") . b),((F ") . c)] in R by A1, A11, A13, A14, Def7;
A16: a in field S by A10, RELAT_1:15;
then A17: a = F . ((F ") . a) by A3, A4, FUNCT_1:35;
 (F ") . a in field R by A2, A3, A5, A16, FUNCT_1:def_3;
then  [((F ") . a),((F ") . b)] in R by A1, A10, A17, A14, Def7;
then  [((F ") . a),((F ") . c)] in R by A9, A15, Lm2;
hence  [a,c] in S by A1, A17, A13, Def7; ::_thesis: verum
end;
hence  S is transitive by Lm2; ::_thesis: verum
end;
thus  ( R is connected implies S is connected ) ::_thesis: ( ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A18: R is connected ; ::_thesis: S is connected
now__::_thesis:_for_a,_b_being_set_st_a_in_field_S_&_b_in_field_S_&_a_<>_b_&_not_[a,b]_in_S_holds_
[b,a]_in_S
let a, b be set ; ::_thesis: ( a in field S & b in field S & a <> b & not [a,b] in S implies [b,a] in S )
assume that
A19: ( a in field S & b in field S ) and
A20: a <> b ; ::_thesis: ( [a,b] in S or [b,a] in S )
A21: ( a = F . ((F ") . a) & b = F . ((F ") . b) ) by A3, A4, A19, FUNCT_1:35;
 ( (F ") . a in field R & (F ") . b in field R ) by A2, A3, A5, A19, FUNCT_1:def_3;
then  ( [((F ") . a),((F ") . b)] in R or [((F ") . b),((F ") . a)] in R ) by A18, A20, A21, Lm4;
hence  ( [a,b] in S or [b,a] in S ) by A1, A21, Def7; ::_thesis: verum
end;
hence  S is connected by Lm4; ::_thesis: verum
end;
thus  ( R is antisymmetric implies S is antisymmetric ) ::_thesis: ( R is well_founded implies S is well_founded )
proof
assume A22: R is antisymmetric ; ::_thesis: S is antisymmetric
now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_S_&_[b,a]_in_S_holds_
a_=_b
let a, b be set ; ::_thesis: ( [a,b] in S & [b,a] in S implies a = b )
assume that
A23: [a,b] in S and
A24: [b,a] in S ; ::_thesis: a = b
A25: a in field S by A23, RELAT_1:15;
then A26: a = F . ((F ") . a) by A3, A4, FUNCT_1:35;
A27: b in field S by A23, RELAT_1:15;
then A28: b = F . ((F ") . b) by A3, A4, FUNCT_1:35;
A29: (F ") . b in field R by A2, A3, A5, A27, FUNCT_1:def_3;
 (F ") . a in field R by A2, A3, A5, A25, FUNCT_1:def_3;
then  ( [((F ") . a),((F ") . b)] in R & [((F ") . b),((F ") . a)] in R ) by A1, A23, A24, A26, A28, A29, Def7;
hence  a = b by A22, A26, A28, Lm3; ::_thesis: verum
end;
hence  S is antisymmetric by Lm3; ::_thesis: verum
end;
assume A30: for Y being set st Y c= field R & Y <> {} holds
ex x being set st
( x in Y & R -Seg x misses Y ) ; :: according to WELLORD1:def_2 ::_thesis: S is well_founded
let Z be set ; :: according to WELLORD1:def_2 ::_thesis: ( Z c= field S & Z <> {} implies ex a being set st
( a in Z & S -Seg a misses Z ) )
assume that
A31: Z c= field S and
A32: Z <> {} ; ::_thesis: ex a being set st
( a in Z & S -Seg a misses Z )
A33: F " Z c= dom F by RELAT_1:132;
then consider x being set  such that
A34: x in F " Z and
A35: R -Seg x misses F " Z by A2, A3, A30, A31, A32, RELAT_1:139;
take  F . x ; ::_thesis: ( F . x in Z & S -Seg (F . x) misses Z )
thus  F . x in Z by A34, FUNCT_1:def_7; ::_thesis: S -Seg (F . x) misses Z
assume  not S -Seg (F . x) misses Z ; ::_thesis: contradiction
then consider y being set  such that
A36: y in S -Seg (F . x) and
A37: y in Z by XBOOLE_0:3;
A38: (F ") . y in dom F by A3, A5, A31, A37, FUNCT_1:def_3;
A39: [y,(F . x)] in S by A36, Th1;
A40: y = F . ((F ") . y) by A3, A4, A31, A37, FUNCT_1:35;
then  (F ") . y in F " Z by A37, A38, FUNCT_1:def_7;
then  not (F ") . y in R -Seg x by A35, XBOOLE_0:3;
then  ( not [((F ") . y),x] in R or (F ") . y = x ) by Th1;
hence  contradiction by A1, A2, A33, A34, A36, A40, A38, A39, Th1, Def7; ::_thesis: verum
end;

theorem Th44: :: WELLORD1:44
for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
S is well-ordering
proof
let R, S be Relation; ::_thesis: for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
S is well-ordering
let F be Function; ::_thesis: ( R is well-ordering & F is_isomorphism_of R,S implies S is well-ordering )
assume  ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded & F is_isomorphism_of R,S ) ; :: according to WELLORD1:def_4 ::_thesis: S is well-ordering
hence  ( S is reflexive & S is transitive & S is antisymmetric & S is connected & S is well_founded ) by Th43; :: according to WELLORD1:def_4 ::_thesis: verum
end;

theorem Th45: :: WELLORD1:45
for R, S being Relation st R is well-ordering holds
for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds
F = G
proof
let R, S be Relation; ::_thesis: ( R is well-ordering implies for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds
F = G )
assume A1: R is well-ordering ; ::_thesis: for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds
F = G
let F, G be Function; ::_thesis: ( F is_isomorphism_of R,S & G is_isomorphism_of R,S implies F = G )
assume that
A2: F is_isomorphism_of R,S and
A3: G is_isomorphism_of R,S ; ::_thesis: F = G
A4: dom F = field R by A2, Def7;
A5: S is well-ordering by A1, A2, Th44;
A6: rng F = field S by A2, Def7;
A7: G is one-to-one by A3, Def7;
A8: dom G = field R by A3, Def7;
A9: G " is_isomorphism_of S,R by A3, Th39;
then A10: G " is one-to-one by Def7;
A11: F is one-to-one by A2, Def7;
A12: rng G = field S by A3, Def7;
A13: F " is_isomorphism_of S,R by A2, Th39;
then A14: F " is one-to-one by Def7;
 for a being set st a in field R holds
F . a = G . a
proof
A15: dom (F ") = field S by A6, A11, FUNCT_1:33;
then A16: dom ((F ") * G) = field R by A8, A12, RELAT_1:27;
A17: now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_R_&_a_<>_b_holds_
(_[(((F_")_*_G)_._a),(((F_")_*_G)_._b)]_in_R_&_((F_")_*_G)_._a_<>_((F_")_*_G)_._b_)
let a, b be set ; ::_thesis: ( [a,b] in R & a <> b implies ( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b ) )
assume that
A18: [a,b] in R and
A19: a <> b ; ::_thesis: ( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b )
A20: [(G . a),(G . b)] in S by A3, A18, Def7;
A21: b in field R by A18, RELAT_1:15;
then A22: (F ") . (G . b) = ((F ") * G) . b by A8, FUNCT_1:13;
A23: a in field R by A18, RELAT_1:15;
then  (F ") . (G . a) = ((F ") * G) . a by A8, FUNCT_1:13;
hence  [(((F ") * G) . a),(((F ") * G) . b)] in R by A13, A20, A22, Def7; ::_thesis: ((F ") * G) . a <> ((F ") * G) . b
thus  ((F ") * G) . a <> ((F ") * G) . b by A14, A7, A16, A19, A23, A21, FUNCT_1:def_4; ::_thesis: verum
end;
A24: dom (G ") = field S by A12, A7, FUNCT_1:33;
then A25: dom ((G ") * F) = field R by A4, A6, RELAT_1:27;
A26: now__::_thesis:_for_a,_b_being_set_st_[a,b]_in_R_&_a_<>_b_holds_
(_[(((G_")_*_F)_._a),(((G_")_*_F)_._b)]_in_R_&_((G_")_*_F)_._a_<>_((G_")_*_F)_._b_)
let a, b be set ; ::_thesis: ( [a,b] in R & a <> b implies ( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b ) )
assume that
A27: [a,b] in R and
A28: a <> b ; ::_thesis: ( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b )
A29: [(F . a),(F . b)] in S by A2, A27, Def7;
A30: b in field R by A27, RELAT_1:15;
then A31: (G ") . (F . b) = ((G ") * F) . b by A4, FUNCT_1:13;
A32: a in field R by A27, RELAT_1:15;
then  (G ") . (F . a) = ((G ") * F) . a by A4, FUNCT_1:13;
hence  [(((G ") * F) . a),(((G ") * F) . b)] in R by A9, A29, A31, Def7; ::_thesis: ((G ") * F) . a <> ((G ") * F) . b
thus  ((G ") * F) . a <> ((G ") * F) . b by A11, A10, A25, A28, A32, A30, FUNCT_1:def_4; ::_thesis: verum
end;
let a be set ; ::_thesis: ( a in field R implies F . a = G . a )
assume A33: a in field R ; ::_thesis: F . a = G . a
A34: (F ") . (G . a) = ((F ") * G) . a by A8, A33, FUNCT_1:13;
 G . a in rng F by A6, A8, A12, A33, FUNCT_1:def_3;
then A35: F . ((F ") . (G . a)) = G . a by A11, FUNCT_1:35;
 rng (F ") = field R by A4, A11, FUNCT_1:33;
then  rng ((F ") * G) = field R by A12, A15, RELAT_1:28;
then  [a,(((F ") * G) . a)] in R by A1, A33, A16, A17, Th35;
then A36: [(F . a),(G . a)] in S by A2, A34, A35, Def7;
 F . a in rng G by A4, A6, A12, A33, FUNCT_1:def_3;
then A37: G . ((G ") . (F . a)) = F . a by A7, FUNCT_1:35;
A38: (G ") . (F . a) = ((G ") * F) . a by A4, A33, FUNCT_1:13;
 rng (G ") = field R by A8, A7, FUNCT_1:33;
then  rng ((G ") * F) = field R by A6, A24, RELAT_1:28;
then  [a,(((G ") * F) . a)] in R by A1, A33, A25, A26, Th35;
then  [(G . a),(F . a)] in S by A3, A38, A37, Def7;
hence  F . a = G . a by A5, A36, Lm3; ::_thesis: verum
end;
hence  F = G by A4, A8, FUNCT_1:2; ::_thesis: verum
end;

definition
let R, S be Relation;
assume that
A1: R is well-ordering and
A2: R,S are_isomorphic ;
func canonical_isomorphism_of (R,S) ->  Function means :Def9: :: WELLORD1:def 9
it is_isomorphism_of R,S;
existence
 ex b1 being Function st b1 is_isomorphism_of R,S by A2, Def8;
uniqueness
 for b1, b2 being Function st b1 is_isomorphism_of R,S & b2 is_isomorphism_of R,S holds
b1 = b2 by A1, Th45;
end;

:: deftheorem Def9 defines canonical_isomorphism_of WELLORD1:def_9_:_
 for R, S being Relation st R is well-ordering & R,S are_isomorphic holds
for b3 being Function holds
( b3 = canonical_isomorphism_of (R,S) iff b3 is_isomorphism_of R,S );

theorem Th46: :: WELLORD1:46
for R being Relation st R is well-ordering holds
for a being set st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
proof
let R be Relation; ::_thesis: ( R is well-ordering implies for a being set st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic )
assume A1: R is well-ordering ; ::_thesis: for a being set st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
let a be set ; ::_thesis: ( a in field R implies not R,R |_2 (R -Seg a) are_isomorphic )
assume A2: a in field R ; ::_thesis: not R,R |_2 (R -Seg a) are_isomorphic
set S = R |_2 (R -Seg a);
set F = canonical_isomorphism_of (R,(R |_2 (R -Seg a)));
assume  R,R |_2 (R -Seg a) are_isomorphic ; ::_thesis: contradiction
then A3: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is_isomorphism_of R,R |_2 (R -Seg a) by A1, Def9;
then A4: dom (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field R by Def7;
A5: canonical_isomorphism_of (R,(R |_2 (R -Seg a))) is one-to-one by A3, Def7;
A6: now__::_thesis:_for_b,_c_being_set_st_[b,c]_in_R_&_b_<>_c_holds_
(_[((canonical_isomorphism_of_(R,(R_|_2_(R_-Seg_a))))_._b),((canonical_isomorphism_of_(R,(R_|_2_(R_-Seg_a))))_._c)]_in_R_&_(canonical_isomorphism_of_(R,(R_|_2_(R_-Seg_a))))_._b_<>_(canonical_isomorphism_of_(R,(R_|_2_(R_-Seg_a))))_._c_)
let b, c be set ; ::_thesis: ( [b,c] in R & b <> c implies ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c ) )
assume that
A7: [b,c] in R and
A8: b <> c ; ::_thesis: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c )
 [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R |_2 (R -Seg a) by A3, A7, Def7;
hence  [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b),((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c)] in R by XBOOLE_0:def_4; ::_thesis: (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c
 ( b in field R & c in field R ) by A7, RELAT_1:15;
hence  (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . b <> (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . c by A4, A5, A8, FUNCT_1:def_4; ::_thesis: verum
end;
A9: rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) = field (R |_2 (R -Seg a)) by A3, Def7;
 field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;
then  (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a in R -Seg a by A2, A4, A9, FUNCT_1:def_3;
then A10: ( [((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a),a] in R & (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a <> a ) by Th1;
 rng (canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) c= field R by A9, Th13;
then  [a,((canonical_isomorphism_of (R,(R |_2 (R -Seg a)))) . a)] in R by A1, A2, A4, A6, Th35;
hence  contradiction by A1, A10, Lm3; ::_thesis: verum
end;

theorem Th47: :: WELLORD1:47
for a, b being set
for R being Relation st R is well-ordering & a in field R & b in field R & a <> b holds
not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
proof
let a, b be set ; ::_thesis: for R being Relation st R is well-ordering & a in field R & b in field R & a <> b holds
not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
let R be Relation; ::_thesis: ( R is well-ordering & a in field R & b in field R & a <> b implies not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic )
assume that
A1: R is well-ordering and
A2: ( a in field R & b in field R ) and
A3: a <> b ; ::_thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
A4: now__::_thesis:_(_R_-Seg_b_c=_R_-Seg_a_implies_not_R_|_2_(R_-Seg_a),R_|_2_(R_-Seg_b)_are_isomorphic_)
set S = R |_2 (R -Seg a);
assume A5: R -Seg b c= R -Seg a ; ::_thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
then A6: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;
A7: field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;
A8: b in R -Seg a
proof
assume  not b in R -Seg a ; ::_thesis: contradiction
then  not [b,a] in R by A3, Th1;
then  [a,b] in R by A2, A3, A1, Lm4;
then  a in R -Seg b by A3, Th1;
hence  contradiction by A5, Th1; ::_thesis: verum
end;
then  R -Seg b = (R |_2 (R -Seg a)) -Seg b by A1, Th27;
hence  not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A1, A7, A8, A6, Th25, Th46; ::_thesis: verum
end;
A9: now__::_thesis:_(_R_-Seg_a_c=_R_-Seg_b_implies_not_R_|_2_(R_-Seg_a),R_|_2_(R_-Seg_b)_are_isomorphic_)
set S = R |_2 (R -Seg b);
assume A10: R -Seg a c= R -Seg b ; ::_thesis: not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
then A11: (R |_2 (R -Seg b)) |_2 (R -Seg a) = R |_2 (R -Seg a) by Th22;
A12: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;
A13: a in R -Seg b
proof
assume  not a in R -Seg b ; ::_thesis: contradiction
then  not [a,b] in R by A3, Th1;
then  [b,a] in R by A2, A3, A1, Lm4;
then  b in R -Seg a by A3, Th1;
hence  contradiction by A10, Th1; ::_thesis: verum
end;
then  R -Seg a = (R |_2 (R -Seg b)) -Seg a by A1, Th27;
hence  not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A13, A11, A12, Th40, Th46; ::_thesis: verum
end;
 R -Seg a,R -Seg b are_c=-comparable by A1, Th26;
hence  not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A9, A4, XBOOLE_0:def_9; ::_thesis: verum
end;

theorem Th48: :: WELLORD1:48
for Z being set
for R, S being Relation
for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
proof
let Z be set ; ::_thesis: for R, S being Relation
for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
let R, S be Relation; ::_thesis: for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
let F be Function; ::_thesis: ( R is well-ordering & Z c= field R & F is_isomorphism_of R,S implies ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: Z c= field R and
A3: F is_isomorphism_of R,S ; ::_thesis: ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
A4: F .: Z c= rng F by RELAT_1:111;
 rng F = field S by A3, Def7;
then A5: F .: Z = field (S |_2 (F .: Z)) by A1, A3, A4, Th31, Th44;
A6: F is one-to-one by A3, Def7;
A7: Z = field (R |_2 Z) by A1, A2, Th31;
A8: dom F = field R by A3, Def7;
thus  F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) ::_thesis: R |_2 Z,S |_2 (F .: Z) are_isomorphic
proof
thus A9: dom (F | Z) = field (R |_2 Z) by A2, A8, A7, RELAT_1:62; :: according to WELLORD1:def_7 ::_thesis: ( rng (F | Z) = field (S |_2 (F .: Z)) & F | Z is one-to-one & ( for a, b being set holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )
thus A10: rng (F | Z) = field (S |_2 (F .: Z)) by A5, RELAT_1:115; ::_thesis: ( F | Z is one-to-one & ( for a, b being set holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )
thus  F | Z is one-to-one by A6, FUNCT_1:52; ::_thesis: for a, b being set holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )
let a, b be set ; ::_thesis: ( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )
thus  ( [a,b] in R |_2 Z implies ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ::_thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) implies [a,b] in R |_2 Z )
proof
assume A11: [a,b] in R |_2 Z ; ::_thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) )
then  [a,b] in R by XBOOLE_0:def_4;
then A12: [(F . a),(F . b)] in S by A3, Def7;
thus A13: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) by A11, RELAT_1:15; ::_thesis: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z)
then  ( (F | Z) . a in rng (F | Z) & (F | Z) . b in rng (F | Z) ) by A9, FUNCT_1:def_3;
then A14: [((F | Z) . a),((F | Z) . b)] in [:(F .: Z),(F .: Z):] by A5, A10, ZFMISC_1:87;
 ( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A13, FUNCT_1:47;
hence  [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) by A12, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
assume that
A15: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) and
A16: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ; ::_thesis: [a,b] in R |_2 Z
 ( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A15, FUNCT_1:47;
then A17: [(F . a),(F . b)] in S by A16, XBOOLE_0:def_4;
A18: [a,b] in [:Z,Z:] by A7, A15, ZFMISC_1:87;
 ( a in field R & b in field R ) by A15, Th12;
then  [a,b] in R by A3, A17, Def7;
hence  [a,b] in R |_2 Z by A18, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  R |_2 Z,S |_2 (F .: Z) are_isomorphic by Def8; ::_thesis: verum
end;

theorem Th49: :: WELLORD1:49
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
proof
let R, S be Relation; ::_thesis: for F being Function st F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
let F be Function; ::_thesis: ( F is_isomorphism_of R,S implies for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A1: F is_isomorphism_of R,S ; ::_thesis: for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
then A2: dom F = field R by Def7;
let a be set ; ::_thesis: ( a in field R implies ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A3: a in field R ; ::_thesis: ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
take b = F . a; ::_thesis: ( b in field S & F .: (R -Seg a) = S -Seg b )
A4: rng F = field S by A1, Def7;
hence  b in field S by A3, A2, FUNCT_1:def_3; ::_thesis: F .: (R -Seg a) = S -Seg b
A5: F is one-to-one by A1, Def7;
A6: for c being set st c in S -Seg b holds
c in F .: (R -Seg a)
proof
let c be set ; ::_thesis: ( c in S -Seg b implies c in F .: (R -Seg a) )
assume A7: c in S -Seg b ; ::_thesis: c in F .: (R -Seg a)
then A8: c <> b by Th1;
A9: [c,b] in S by A7, Th1;
then A10: c in field S by RELAT_1:15;
then A11: c = F . ((F ") . c) by A4, A5, FUNCT_1:35;
 ( rng (F ") = dom F & dom (F ") = rng F ) by A5, FUNCT_1:33;
then A12: (F ") . c in field R by A2, A4, A10, FUNCT_1:def_3;
then  [((F ") . c),a] in R by A1, A3, A9, A11, Def7;
then  (F ") . c in R -Seg a by A8, A11, Th1;
hence  c in F .: (R -Seg a) by A2, A11, A12, FUNCT_1:def_6; ::_thesis: verum
end;
 for c being set st c in F .: (R -Seg a) holds
c in S -Seg b
proof
let c be set ; ::_thesis: ( c in F .: (R -Seg a) implies c in S -Seg b )
assume  c in F .: (R -Seg a) ; ::_thesis: c in S -Seg b
then consider d being set  such that
A13: d in dom F and
A14: d in R -Seg a and
A15: c = F . d by FUNCT_1:def_6;
 [d,a] in R by A14, Th1;
then A16: [c,b] in S by A1, A15, Def7;
 d <> a by A14, Th1;
then  c <> b by A3, A2, A5, A13, A15, FUNCT_1:def_4;
hence  c in S -Seg b by A16, Th1; ::_thesis: verum
end;
hence  F .: (R -Seg a) = S -Seg b by A6, TARSKI:1; ::_thesis: verum
end;

theorem Th50: :: WELLORD1:50
for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
proof
let R, S be Relation; ::_thesis: for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
let F be Function; ::_thesis: ( R is well-ordering & F is_isomorphism_of R,S implies for a being set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: F is_isomorphism_of R,S ; ::_thesis: for a being set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
let a be set ; ::_thesis: ( a in field R implies ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )
assume  a in field R ; ::_thesis: ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
then consider b being set  such that
A3: ( b in field S & F .: (R -Seg a) = S -Seg b ) by A2, Th49;
take  b ; ::_thesis: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
 R -Seg a c= field R by Th9;
hence  ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A1, A2, A3, Th48; ::_thesis: verum
end;

theorem Th51: :: WELLORD1:51
for a, b, c being set
for R, S being Relation st R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic holds
( S -Seg c c= S -Seg b & [c,b] in S )
proof
let a, b, c be set ; ::_thesis: for R, S being Relation st R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic holds
( S -Seg c c= S -Seg b & [c,b] in S )
let R, S be Relation; ::_thesis: ( R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic implies ( S -Seg c c= S -Seg b & [c,b] in S ) )
assume that
A1: R is well-ordering and
A2: S is well-ordering and
A3: a in field R and
A4: b in field S and
A5: c in field S and
A6: R,S |_2 (S -Seg b) are_isomorphic and
A7: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ; ::_thesis: ( S -Seg c c= S -Seg b & [c,b] in S )
set Q = S |_2 (S -Seg b);
set F1 = canonical_isomorphism_of (R,(S |_2 (S -Seg b)));
A8: canonical_isomorphism_of (R,(S |_2 (S -Seg b))) is_isomorphism_of R,S |_2 (S -Seg b) by A1, A6, Def9;
then consider d being set  such that
A9: d in field (S |_2 (S -Seg b)) and
A10: (canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) .: (R -Seg a) = (S |_2 (S -Seg b)) -Seg d by A3, Th49;
A11: S -Seg b = field (S |_2 (S -Seg b)) by A2, Th32;
then A12: (S |_2 (S -Seg b)) -Seg d = S -Seg d by A2, A9, Th27;
A13: rng (canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) = S -Seg b by A8, A11, Def7;
then A14: (S |_2 (S -Seg b)) -Seg d c= S -Seg b by A10, RELAT_1:111;
set T = S |_2 (S -Seg c);
set P = R |_2 (R -Seg a);
A15: S |_2 (S -Seg c),R |_2 (R -Seg a) are_isomorphic by A7, Th40;
A16: d in field S by A9, Th12;
 R -Seg a c= field R by Th9;
then  R |_2 (R -Seg a),(S |_2 (S -Seg b)) |_2 ((canonical_isomorphism_of (R,(S |_2 (S -Seg b)))) .: (R -Seg a)) are_isomorphic by A1, A8, Th48;
then  S |_2 (S -Seg c),(S |_2 (S -Seg b)) |_2 ((S |_2 (S -Seg b)) -Seg d) are_isomorphic by A10, A15, Th42;
then  S |_2 (S -Seg c),S |_2 (S -Seg d) are_isomorphic by A10, A12, A13, Th22, RELAT_1:111;
hence  S -Seg c c= S -Seg b by A2, A5, A12, A14, A16, Th47; ::_thesis: [c,b] in S
hence  [c,b] in S by A2, A4, A5, Th29; ::_thesis: verum
end;

theorem Th52: :: WELLORD1:52
for R, S being Relation st R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being set holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) holds
ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
proof
let R, S be Relation; ::_thesis: ( R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being set holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) implies ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: S is well-ordering ; ::_thesis: ( R,S are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
defpred S1[ set ] means  ex b being set st
( b in field S & R |_2 (R -Seg $1),S |_2 (S -Seg b) are_isomorphic );
consider Z being set  such that
A3: for a being set holds
( a in Z iff ( a in field R & S1[a] ) ) from XBOOLE_0:sch_1();
A4: Z c= field R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in field R )
thus  ( not x in Z or x in field R ) by A3; ::_thesis: verum
end;
defpred S2[ set , set ] means ( $2 in field S & R |_2 (R -Seg $1),S |_2 (S -Seg $2) are_isomorphic );
A5: for a, b, c being set st S2[a,b] & S2[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S2[a,b] & S2[a,c] implies b = c )
assume that
A6: b in field S and
A7: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic and
A8: ( c in field S & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ) ; ::_thesis: b = c
 S |_2 (S -Seg b),R |_2 (R -Seg a) are_isomorphic by A7, Th40;
hence  b = c by A2, A6, A8, Th42, Th47; ::_thesis: verum
end;
consider F being Function such that
A9: for a, b being set holds
( [a,b] in F iff ( a in field R & S2[a,b] ) ) from FUNCT_1:sch_1(A5);
A10: Z = dom F
proof
thus  for a being set st a in Z holds
a in dom F :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: dom F c= Z
proof
let a be set ; ::_thesis: ( a in Z implies a in dom F )
assume A11: a in Z ; ::_thesis: a in dom F
then consider b being set  such that
A12: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A3;
 a in field R by A3, A11;
then  [a,b] in F by A9, A12;
hence  a in dom F by XTUPLE_0:def_12; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom F or a in Z )
assume  a in dom F ; ::_thesis: a in Z
then consider b being set  such that
A13: [a,b] in F by XTUPLE_0:def_12;
A14: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A9, A13;
 ( a in field R & b in field S ) by A9, A13;
hence  a in Z by A3, A14; ::_thesis: verum
end;
A15: rng F c= field S
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng F or a in field S )
assume  a in rng F ; ::_thesis: a in field S
then consider b being set  such that
A16: ( b in dom F & a = F . b ) by FUNCT_1:def_3;
 [b,a] in F by A16, FUNCT_1:1;
hence  a in field S by A9; ::_thesis: verum
end;
A17: F is_isomorphism_of R |_2 (dom F),S |_2 (rng F)
proof
thus  ( dom F = field (R |_2 (dom F)) & rng F = field (S |_2 (rng F)) ) by A1, A2, A4, A15, A10, Th31; :: according to WELLORD1:def_7 ::_thesis: ( F is one-to-one & ( for a, b being set holds
( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) ) )
thus A18: F is one-to-one ::_thesis: for a, b being set holds
( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom F or not b1 in dom F or not F . a = F . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom F or not b in dom F or not F . a = F . b or a = b )
assume that
A19: a in dom F and
A20: b in dom F and
A21: F . a = F . b ; ::_thesis: a = b
A22: [b,(F . b)] in F by A20, FUNCT_1:1;
then  R |_2 (R -Seg b),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A21;
then A23: S |_2 (S -Seg (F . a)),R |_2 (R -Seg b) are_isomorphic by Th40;
 [a,(F . a)] in F by A19, FUNCT_1:1;
then A24: ( a in field R & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9;
 b in field R by A9, A22;
hence  a = b by A1, A24, A23, Th42, Th47; ::_thesis: verum
end;
let a, b be set ; ::_thesis: ( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )
set P = R |_2 (R -Seg a);
A25: ( field (R |_2 (R -Seg a)) = R -Seg a & R |_2 (R -Seg a) is well-ordering ) by A1, Th25, Th32;
thus  ( [a,b] in R |_2 (dom F) implies ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) ::_thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) implies [a,b] in R |_2 (dom F) )
proof
assume A26: [a,b] in R |_2 (dom F) ; ::_thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) )
hence A27: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) ) by RELAT_1:15; ::_thesis: [(F . a),(F . b)] in S |_2 (rng F)
then A28: a in dom F by Th12;
then A29: [a,(F . a)] in F by FUNCT_1:1;
then A30: F . a in field S by A9;
A31: b in dom F by A27, Th12;
then A32: [b,(F . b)] in F by FUNCT_1:1;
then A33: b in field R by A9;
A34: ( F . b in field S & R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic ) by A9, A32;
A35: [a,b] in R by A26, XBOOLE_0:def_4;
A36: F . b in rng F by A31, FUNCT_1:def_3;
 F . a in rng F by A28, FUNCT_1:def_3;
then A37: [(F . a),(F . b)] in [:(rng F),(rng F):] by A36, ZFMISC_1:87;
 a in field R by A9, A29;
then A38: R -Seg a c= R -Seg b by A1, A33, A35, Th29;
A39: R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A29;
A40: now__::_thesis:_(_a_<>_b_implies_[(F_._a),(F_._b)]_in_S_|_2_(rng_F)_)
set P = R |_2 (R -Seg b);
A41: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;
assume  a <> b ; ::_thesis: [(F . a),(F . b)] in S |_2 (rng F)
then A42: a in R -Seg b by A35, Th1;
then  (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, Th27;
then  (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A39, A38, Th22;
then  [(F . a),(F . b)] in S by A2, A30, A34, A42, A41, Th51;
hence  [(F . a),(F . b)] in S |_2 (rng F) by A37, XBOOLE_0:def_4; ::_thesis: verum
end;
 ( a = b implies [(F . a),(F . b)] in S |_2 (rng F) )
proof
assume  a = b ; ::_thesis: [(F . a),(F . b)] in S |_2 (rng F)
then  [(F . a),(F . b)] in S by A2, A30, Lm1;
hence  [(F . a),(F . b)] in S |_2 (rng F) by A37, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  [(F . a),(F . b)] in S |_2 (rng F) by A40; ::_thesis: verum
end;
assume that
A43: a in field (R |_2 (dom F)) and
A44: b in field (R |_2 (dom F)) and
A45: [(F . a),(F . b)] in S |_2 (rng F) ; ::_thesis: [a,b] in R |_2 (dom F)
A46: [(F . a),(F . b)] in S by A45, XBOOLE_0:def_4;
A47: a in dom F by A43, Th12;
then A48: [a,(F . a)] in F by FUNCT_1:1;
then A49: a in field R by A9;
assume  not [a,b] in R |_2 (dom F) ; ::_thesis: contradiction
then A50: ( not [a,b] in R or not [a,b] in [:(dom F),(dom F):] ) by XBOOLE_0:def_4;
then A51: a <> b by A1, A47, A49, Lm1, ZFMISC_1:87;
A52: b in dom F by A44, Th12;
then A53: [b,(F . b)] in F by FUNCT_1:1;
then A54: R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A9;
A55: b in field R by A9, A53;
then A56: [b,a] in R by A1, A47, A52, A50, A49, A51, Lm4, ZFMISC_1:87;
then A57: R -Seg b c= R -Seg a by A1, A49, A55, Th29;
A58: b in R -Seg a by A47, A52, A50, A56, Th1, ZFMISC_1:87;
then  (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;
then A59: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A54, A57, Th22;
A60: F . b in field S by A9, A53;
 ( F . a in field S & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9, A48;
then  [(F . b),(F . a)] in S by A2, A60, A58, A25, A59, Th51;
then  F . a = F . b by A2, A46, Lm3;
hence  contradiction by A18, A47, A52, A51, FUNCT_1:def_4; ::_thesis: verum
end;
A61: now__::_thesis:_(_ex_a_being_set_st_
(_a_in_field_R_&_Z_=_R_-Seg_a_)_implies_for_b_being_set_holds_
(_not_b_in_field_S_or_not_rng_F_=_S_-Seg_b_)_)
given a being set  such that A62: a in field R and
A63: Z = R -Seg a ; ::_thesis: for b being set holds
( not b in field S or not rng F = S -Seg b )
given b being set  such that A64: b in field S and
A65: rng F = S -Seg b ; ::_thesis: contradiction
 R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A10, A17, A63, A65, Def8;
then  a in Z by A3, A62, A64;
hence  contradiction by A63, Th1; ::_thesis: verum
end;
A66: now__::_thesis:_for_a_being_set_st_a_in_Z_holds_
for_b_being_set_st_[b,a]_in_R_holds_
b_in_Z
let a be set ; ::_thesis: ( a in Z implies for b being set st [b,a] in R holds
b in Z )
assume A67: a in Z ; ::_thesis: for b being set st [b,a] in R holds
b in Z
consider c being set  such that
A68: c in field S and
A69: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic by A3, A67;
let b be set ; ::_thesis: ( [b,a] in R implies b in Z )
assume A70: [b,a] in R ; ::_thesis: b in Z
A71: a in field R by A3, A67;
now__::_thesis:_(_a_<>_b_implies_b_in_Z_)
set Q = S |_2 (S -Seg c);
set P = R |_2 (R -Seg a);
 R |_2 (R -Seg a) is well-ordering by A1, Th25;
then A72: canonical_isomorphism_of ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) is_isomorphism_of R |_2 (R -Seg a),S |_2 (S -Seg c) by A69, Def9;
assume  a <> b ; ::_thesis: b in Z
then A73: b in R -Seg a by A70, Th1;
then A74: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;
A75: b in field R by A70, RELAT_1:15;
then  R -Seg b c= R -Seg a by A1, A71, A73, Th30;
then A76: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;
 field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;
then consider d being set  such that
A77: d in field (S |_2 (S -Seg c)) and
A78: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(S |_2 (S -Seg c)) |_2 ((S |_2 (S -Seg c)) -Seg d) are_isomorphic by A1, A72, A73, Th25, Th50;
A79: S -Seg c = field (S |_2 (S -Seg c)) by A2, Th32;
then A80: (S |_2 (S -Seg c)) -Seg d = S -Seg d by A2, A77, Th27;
 [d,c] in S by A77, A79, Th1;
then A81: d in field S by RELAT_1:15;
then  S -Seg d c= S -Seg c by A2, A68, A77, A79, Th30;
then  R |_2 (R -Seg b),S |_2 (S -Seg d) are_isomorphic by A78, A74, A80, A76, Th22;
hence  b in Z by A3, A75, A81; ::_thesis: verum
end;
hence  b in Z by A67; ::_thesis: verum
end;
A82: R |_2 Z,S |_2 (rng F) are_isomorphic by A10, A17, Def8;
A83: now__::_thesis:_(_Z_=_field_R_&_ex_a_being_set_st_
(_a_in_field_S_&_rng_F_=_S_-Seg_a_)_implies_ex_a_being_set_st_
(_a_in_field_S_&_R,S_|_2_(S_-Seg_a)_are_isomorphic_)_)
assume A84: Z = field R ; ::_thesis: ( ex a being set st
( a in field S & rng F = S -Seg a ) implies ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
given a being set  such that A85: a in field S and
A86: rng F = S -Seg a ; ::_thesis: ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
take a = a; ::_thesis: ( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
thus  a in field S by A85; ::_thesis: R,S |_2 (S -Seg a) are_isomorphic
thus  R,S |_2 (S -Seg a) are_isomorphic by A82, A84, A86, Th23; ::_thesis: verum
end;
A87: now__::_thesis:_for_a_being_set_st_a_in_rng_F_holds_
for_b_being_set_st_[b,a]_in_S_holds_
b_in_rng_F
let a be set ; ::_thesis: ( a in rng F implies for b being set st [b,a] in S holds
b in rng F )
assume A88: a in rng F ; ::_thesis: for b being set st [b,a] in S holds
b in rng F
consider c being set  such that
A89: ( c in dom F & a = F . c ) by A88, FUNCT_1:def_3;
A90: [c,a] in F by A89, FUNCT_1:1;
then A91: a in field S by A9;
let b be set ; ::_thesis: ( [b,a] in S implies b in rng F )
assume A92: [b,a] in S ; ::_thesis: b in rng F
A93: R |_2 (R -Seg c),S |_2 (S -Seg a) are_isomorphic by A9, A90;
A94: c in field R by A9, A90;
now__::_thesis:_(_a_<>_b_implies_b_in_rng_F_)
set Q = S |_2 (S -Seg a);
set P = R |_2 (R -Seg c);
assume  a <> b ; ::_thesis: b in rng F
then A95: b in S -Seg a by A92, Th1;
then A96: (S |_2 (S -Seg a)) -Seg b = S -Seg b by A2, Th27;
A97: b in field S by A92, RELAT_1:15;
then  S -Seg b c= S -Seg a by A2, A91, A95, Th30;
then A98: (S |_2 (S -Seg a)) |_2 (S -Seg b) = S |_2 (S -Seg b) by Th22;
 ( S |_2 (S -Seg a),R |_2 (R -Seg c) are_isomorphic & S |_2 (S -Seg a) is well-ordering ) by A2, A93, Th25, Th40;
then A99: canonical_isomorphism_of ((S |_2 (S -Seg a)),(R |_2 (R -Seg c))) is_isomorphism_of S |_2 (S -Seg a),R |_2 (R -Seg c) by Def9;
 field (S |_2 (S -Seg a)) = S -Seg a by A2, Th32;
then consider d being set  such that
A100: d in field (R |_2 (R -Seg c)) and
A101: (S |_2 (S -Seg a)) |_2 ((S |_2 (S -Seg a)) -Seg b),(R |_2 (R -Seg c)) |_2 ((R |_2 (R -Seg c)) -Seg d) are_isomorphic by A2, A99, A95, Th25, Th50;
A102: R -Seg c = field (R |_2 (R -Seg c)) by A1, Th32;
then A103: (R |_2 (R -Seg c)) -Seg d = R -Seg d by A1, A100, Th27;
 [d,c] in R by A100, A102, Th1;
then A104: d in field R by RELAT_1:15;
then  R -Seg d c= R -Seg c by A1, A94, A100, A102, Th30;
then  S |_2 (S -Seg b),R |_2 (R -Seg d) are_isomorphic by A101, A96, A103, A98, Th22;
then  R |_2 (R -Seg d),S |_2 (S -Seg b) are_isomorphic by Th40;
then  [d,b] in F by A9, A97, A104;
then  ( d in dom F & b = F . d ) by FUNCT_1:1;
hence  b in rng F by FUNCT_1:def_3; ::_thesis: verum
end;
hence  b in rng F by A88; ::_thesis: verum
end;
A105: now__::_thesis:_(_rng_F_=_field_S_&_ex_a_being_set_st_
(_a_in_field_R_&_Z_=_R_-Seg_a_)_implies_ex_a_being_set_st_
(_a_in_field_R_&_R_|_2_(R_-Seg_a),S_are_isomorphic_)_)
assume A106: rng F = field S ; ::_thesis: ( ex a being set st
( a in field R & Z = R -Seg a ) implies ex a being set st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )
given a being set  such that A107: a in field R and
A108: Z = R -Seg a ; ::_thesis: ex a being set st
( a in field R & R |_2 (R -Seg a),S are_isomorphic )
take a = a; ::_thesis: ( a in field R & R |_2 (R -Seg a),S are_isomorphic )
thus  a in field R by A107; ::_thesis: R |_2 (R -Seg a),S are_isomorphic
thus  R |_2 (R -Seg a),S are_isomorphic by A82, A106, A108, Th23; ::_thesis: verum
end;
now__::_thesis:_(_Z_=_field_R_&_rng_F_=_field_S_implies_R,S_are_isomorphic_)
assume A109: ( Z = field R & rng F = field S ) ; ::_thesis: R,S are_isomorphic
 ( R |_2 (field R) = R & S |_2 (field S) = S ) by Th23;
hence  R,S are_isomorphic by A10, A17, A109, Def8; ::_thesis: verum
end;
hence  ( R,S are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) ) by A1, A2, A4, A15, A66, A87, A61, A83, A105, Th28; ::_thesis: verum
end;

theorem :: WELLORD1:53
for Y being set
for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds
ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )
proof
let Y be set ; ::_thesis: for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds
ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )
let R be Relation; ::_thesis: ( Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic implies ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) )
assume that
A1: Y c= field R and
A2: R is well-ordering ; ::_thesis: ( R,R |_2 Y are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) )
A3: now__::_thesis:_for_a_being_set_holds_
(_not_a_in_field_(R_|_2_Y)_or_not_R,(R_|_2_Y)_|_2_((R_|_2_Y)_-Seg_a)_are_isomorphic_)
given a being set  such that A4: a in field (R |_2 Y) and
A5: R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) are_isomorphic ; ::_thesis: contradiction
consider F being Function such that
A6: F is_isomorphism_of R,(R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A5, Def8;
A7: now__::_thesis:_for_c,_b_being_set_st_[c,b]_in_R_&_c_<>_b_holds_
(_[(F_._c),(F_._b)]_in_R_&_F_._c_<>_F_._b_)
let c, b be set ; ::_thesis: ( [c,b] in R & c <> b implies ( [(F . c),(F . b)] in R & F . c <> F . b ) )
assume A8: ( [c,b] in R & c <> b ) ; ::_thesis: ( [(F . c),(F . b)] in R & F . c <> F . b )
then  [(F . c),(F . b)] in (R |_2 Y) |_2 ((R |_2 Y) -Seg a) by A6, Th36;
then  [(F . c),(F . b)] in R |_2 Y by XBOOLE_0:def_4;
hence  ( [(F . c),(F . b)] in R & F . c <> F . b ) by A6, A8, Th36, XBOOLE_0:def_4; ::_thesis: verum
end;
A9: field (R |_2 Y) = Y by A1, A2, Th31;
 field ((R |_2 Y) |_2 ((R |_2 Y) -Seg a)) = (R |_2 Y) -Seg a by A2, Th25, Th32;
then A10: rng F = (R |_2 Y) -Seg a by A6, Def7;
A11: dom F = field R by A6, Def7;
then A12: F . a in rng F by A1, A4, A9, FUNCT_1:def_3;
then A13: F . a <> a by A10, Th1;
 [(F . a),a] in R |_2 Y by A10, A12, Th1;
then A14: [(F . a),a] in R by XBOOLE_0:def_4;
 (R |_2 Y) -Seg a c= Y by A9, Th9;
then  rng F c= field R by A1, A10, XBOOLE_1:1;
then  [a,(F . a)] in R by A1, A2, A4, A9, A11, A7, Th35;
hence  contradiction by A13, A14, A2, Lm3; ::_thesis: verum
end;
 R |_2 Y is well-ordering by A2, Th25;
hence  ( R,R |_2 Y are_isomorphic or ex a being set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) ) by A2, A3, Th52; ::_thesis: verum
end;

theorem :: WELLORD1:54
for R, S being Relation st R,S are_isomorphic & R is well-ordering holds
S is well-ordering
proof
let R, S be Relation; ::_thesis: ( R,S are_isomorphic & R is well-ordering implies S is well-ordering )
assume  R,S are_isomorphic ; ::_thesis: ( not R is well-ordering or S is well-ordering )
then  ex F being Function st F is_isomorphism_of R,S by Def8;
hence  ( not R is well-ordering or S is well-ordering ) by Th44; ::_thesis: verum
end;