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₁[ object , object ] means [(f . $1),(f . $2)] in R;
consider Q being Relation such that
A5: for x, y being object 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
A6: R is_reflexive_in field R by A1, 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 object ; :: 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 object holds not [y,x] in Q by A5, A9;
then A10: not x in rng Q by XTUPLE_0:def 13;
for y being object holds not [x,y] in Q by A5, A9;
then not x in dom Q by XTUPLE_0:def 12;
hence contradiction by A8, A10, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: 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;
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 by A2, A3, A4, A7, A5;
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