let R, S be Relation; :: thesis: ( R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being object holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) implies ex a being object 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 object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

defpred S1[ object ] means ex b being object 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 object holds
( a in Z iff ( a in field R & S1[a] ) ) from A4: Z c= field R by A3;
defpred S2[ object , object ] means ( \$2 in field S & R |_2 (R -Seg \$1),S |_2 (S -Seg \$2) are_isomorphic );
A5: for a, b, c being object st S2[a,b] & S2[a,c] holds
b = c
proof
let a, b, c be object ; :: 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 ;
hence b = c by A2, A6, A8, Th42, Th47; :: thesis: verum
end;
consider F being Function such that
A9: for a, b being object holds
( [a,b] in F iff ( a in field R & S2[a,b] ) ) from A10: Z = dom F
proof
thus for a being object 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 object ; :: thesis: ( a in Z implies a in dom F )
assume A11: a in Z ; :: thesis: a in dom F
then consider b being object 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 ;
then [a,b] in F by ;
hence a in dom F by XTUPLE_0:def 12; :: thesis: verum
end;
let a be object ; :: 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 object 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 ;
( a in field R & b in field S ) by ;
hence a in Z by ; :: thesis: verum
end;
A15: rng F c= field S
proof
let a be object ; :: 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 object such that
A16: ( b in dom F & a = F . b ) by FUNCT_1:def 3;
[b,a] in F by ;
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 object 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 object 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, b be object ; :: according to FUNCT_1:def 4 :: 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 ;
then R |_2 (R -Seg b),S |_2 (S -Seg (F . a)) are_isomorphic by ;
then A23: S |_2 (S -Seg (F . a)),R |_2 (R -Seg b) are_isomorphic by Th40;
[a,(F . a)] in F by ;
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 ;
hence a = b by A1, A24, A23, Th42, Th47; :: thesis: verum
end;
let a, b be object ; :: 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 ;
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 ;
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 ;
A35: [a,b] in R by ;
A36: F . b in rng F by ;
F . a in rng F by ;
then A37: [(F . a),(F . b)] in [:(rng F),(rng F):] by ;
a in field R by ;
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 ;
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 ;
assume a <> b ; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)
then A42: a in R -Seg b by ;
then (R |_2 (R -Seg b)) -Seg a = R -Seg a by ;
then (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by ;
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 ; :: 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 ; :: 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 ;
A47: a in dom F by ;
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 ;
A52: b in dom F by ;
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 ;
then A56: [b,a] in R by ;
then A57: R -Seg b c= R -Seg a by A1, A49, A55, Th29;
A58: b in R -Seg a by ;
then (R |_2 (R -Seg a)) -Seg b = R -Seg b by ;
then A59: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by ;
A60: F . b in field S by ;
( F . a in field S & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by ;
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; :: thesis: verum
end;
A61: now :: thesis: ( ex a being object st
( a in field R & Z = R -Seg a ) implies for b being object holds
( not b in field S or not rng F = S -Seg b ) )
given a being object such that A62: a in field R and
A63: Z = R -Seg a ; :: thesis: for b being object holds
( not b in field S or not rng F = S -Seg b )

given b being object 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;
then a in Z by A3, A62, A64;
hence contradiction by A63, Th1; :: thesis: verum
end;
A66: now :: thesis: for a being object st a in Z holds
for b being object st [b,a] in R holds
b in Z
let a be object ; :: thesis: ( a in Z implies for b being object st [b,a] in R holds
b in Z )

assume A67: a in Z ; :: thesis: for b being object st [b,a] in R holds
b in Z

consider c being object such that
A68: c in field S and
A69: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic by ;
let b be object ; :: 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 ;
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 ;
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 ;
assume a <> b ; :: thesis: b in Z
then A73: b in R -Seg a by ;
then A74: (R |_2 (R -Seg a)) -Seg b = R -Seg b by ;
A75: b in field R by ;
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 ;
then consider d being object 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 ;
then A80: (S |_2 (S -Seg c)) -Seg d = S -Seg d by ;
[d,c] in S by ;
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 ;
A83: now :: thesis: ( Z = field R & ex a being object st
( a in field S & rng F = S -Seg a ) implies ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
assume A84: Z = field R ; :: thesis: ( ex a being object st
( a in field S & rng F = S -Seg a ) implies ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

given a being object such that A85: a in field S and
A86: rng F = S -Seg a ; :: thesis: ex a being object 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 ; :: thesis: verum
end;
A87: now :: thesis: for a being object st a in rng F holds
for b being object st [b,a] in S holds
b in rng F
let a be object ; :: thesis: ( a in rng F implies for b being object st [b,a] in S holds
b in rng F )

assume A88: a in rng F ; :: thesis: for b being object st [b,a] in S holds
b in rng F

consider c being object such that
A89: ( c in dom F & a = F . c ) by ;
A90: [c,a] in F by ;
then A91: a in field S by A9;
let b be object ; :: 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 ;
A94: c in field R by ;
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 ;
then A96: (S |_2 (S -Seg a)) -Seg b = S -Seg b by ;
A97: b in field S by ;
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 ;
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 ;
then consider d being object 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 ;
then A103: (R |_2 (R -Seg c)) -Seg d = R -Seg d by ;
[d,c] in R by ;
then A104: d in field R by RELAT_1:15;
then R -Seg d c= R -Seg c by ;
then S |_2 (S -Seg b),R |_2 (R -Seg d) are_isomorphic by ;
then R |_2 (R -Seg d),S |_2 (S -Seg b) are_isomorphic by Th40;
then [d,b] in F by ;
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 object st
( a in field R & Z = R -Seg a ) implies ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )
assume A106: rng F = field S ; :: thesis: ( ex a being object st
( a in field R & Z = R -Seg a ) implies ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )

given a being object such that A107: a in field R and
A108: Z = R -Seg a ; :: thesis: ex a being object 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 ; :: 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 |_2 () = R & S |_2 () = S ) by Th23;
hence R,S are_isomorphic by ; :: thesis: verum
end;
hence ( R,S are_isomorphic or ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object 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