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 )
then R is reflexive by WELLORD1:def 4;
then A2: R is_reflexive_in field R by RELAT_2:def 9;
given f being Function such that A3: ( f is one-to-one & dom f = X & 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
A4: 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();
A5: 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 A6: ( x in field Q & not x in X ) ; :: thesis: contradiction
then ( ( for y being set holds not [x,y] in Q ) & ( for y being set holds not [y,x] in Q ) ) by A4;
then ( not x in dom Q & not x in rng Q ) by RELAT_1:def 4, RELAT_1:def 5;
hence contradiction by A6, 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 A7: x in X ; :: thesis: x in field Q
then f . x in rng f by A3, FUNCT_1:def 5;
then [(f . x),(f . x)] in R by A2, A3, RELAT_2:def 1;
then [x,x] in Q by A4, A7;
hence x in field Q by RELAT_1:30; :: 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 A3, A5; :: 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 A4, A5; :: 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 A4, A5; :: thesis: verum

end;

then f " is_isomorphism_of R,Q by WELLORD1:49;
then A8: Q is well-ordering by A1, WELLORD1:54;
take Q ; :: thesis: Q well_orders X
thus Q well_orders X by A5, A8, WELLORD1:8; :: thesis: verum