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_{1}[ 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_{1}[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

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

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

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

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

f is_isomorphism_of Q,R
by A2, A3, A4, A7, A5;
thus
field Q c= X
:: according to XBOOLE_0:def 10 :: thesis: X c= 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field Q )
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;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

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

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