let X be set ; :: thesis: for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X
let R be Relation; :: thesis: ( R is well-ordering & X, field R are_equipotent implies ex R being Relation st R well_orders X )
assume A1: R is well-ordering ; :: thesis: ( not X, field R are_equipotent or ex R being Relation st R well_orders X )
given f being Function such that A2: f is one-to-one and
A3: dom f = X and
A4: rng f = field R ; :: according to WELLORD2:def 4 :: thesis: ex R being Relation st R well_orders X
defpred S₁[ set , set ] means [(f . $1),(f . $2)] in R;
consider Q being Relation such that
A5: for x, y being set holds
( [x,y] in Q iff ( x in X & y in X & S₁[x,y] ) ) from RELAT_1:sch 1();
take Q ; :: thesis: Q well_orders X
R is reflexive by A1, WELLORD1:def 4;
then A6: R is_reflexive_in field R by RELAT_2:def 9;
A7: field Q = X

proof

thus field Q c= X :: according to XBOOLE_0:def 10 :: thesis: X c= field Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in field Q or x in X )
assume that
A8: x in field Q and
A9: not x in X ; :: thesis: contradiction
for y being set holds not [y,x] in Q by A5, A9;
then A10: not x in rng Q by RELAT_1:def 5;
for y being set holds not [x,y] in Q by A5, A9;
then not x in dom Q by RELAT_1:def 4;
hence contradiction by A8, A10, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field Q )
assume A11: x in X ; :: thesis: x in field Q
then f . x in rng f by A3, FUNCT_1:def 3;
then [(f . x),(f . x)] in R by A6, A4, RELAT_2:def 1;
then [x,x] in Q by A5, A11;
hence x in field Q by RELAT_1:15; :: thesis: verum

end;

f is_isomorphism_of Q,R

proof

thus ( dom f = field Q & rng f = field R & f is one-to-one ) by A2, A3, A4, A7; :: according to WELLORD1:def 7 :: thesis: for b₁, b₂ being set holds
( ( not [b₁,b₂] in Q or ( b₁ in field Q & b₂ in field Q & [(f . b₁),(f . b₂)] in R ) ) & ( not b₁ in field Q or not b₂ in field Q or not [(f . b₁),(f . b₂)] in R or [b₁,b₂] in Q ) )
let x, y be set ; :: thesis: ( ( not [x,y] in Q or ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ) & ( not x in field Q or not y in field Q or not [(f . x),(f . y)] in R or [x,y] in Q ) )
thus ( [x,y] in Q implies ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ) by A5, A7; :: thesis: ( not x in field Q or not y in field Q or not [(f . x),(f . y)] in R or [x,y] in Q )
assume ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ; :: thesis: [x,y] in Q
hence [x,y] in Q by A5, A7; :: thesis: verum

end;

then f " is_isomorphism_of R,Q by WELLORD1:39;
then Q is well-ordering by A1, WELLORD1:44;
hence Q well_orders X by A7, WELLORD1:4; :: thesis: verum