let X be set ; :: thesis: for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )

let A be Ordinal; :: thesis: ( X,A are_equipotent implies ex R being Order of X st
( R well_orders X & order_type_of R = A ) )

given f being Function such that A1: f is one-to-one and
A2: dom f = X and
A3: rng f = A ; :: according to WELLORD2:def 4 :: thesis: ex R being Order of X st
( R well_orders X & order_type_of R = A )

reconsider f = f as Function of X,A by ;
reconsider g = f " as Function of A,X by ;
A4: dom g = A by ;
reconsider f9 = f as one-to-one Function by A1;
A5: dom () = A by ORDERS_1:14;
rng () = A by ORDERS_1:14;
then A6: rng (f * ()) = A by ;
set R = (f * ()) * g;
dom (f * ()) = X by ;
then A7: dom ((f * ()) * g) = X by ;
rng g = X by ;
then rng ((f * ()) * g) = X by ;
then A8: field ((f * ()) * g) = X \/ X by
.= X ;
reconsider R = (f * ()) * g as Relation of X ;
(f9 * ()) * (f9 ") is_reflexive_in X by ;
then reconsider R = R as Order of X by ;
A9: f is_isomorphism_of R, RelIncl A
proof
thus ( dom f = field R & rng f = field () & f is one-to-one ) by ; :: according to WELLORD1:def 7 :: thesis: for b1, b2 being object holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(f . b1),(f . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(f . b1),(f . b2)] in RelIncl A or [b1,b2] in R ) )

let a, b be object ; :: thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) )
hereby :: thesis: ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R )
assume A10: [a,b] in R ; :: thesis: ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A )
hence ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [(f . a),(f . b)] in RelIncl A
consider x being object such that
A11: [a,x] in f * () and
A12: [x,b] in g by ;
A13: ( b = g . x & x in dom g ) by ;
consider y being object such that
A14: [a,y] in f and
A15: [y,x] in RelIncl A by ;
y = f . a by ;
hence [(f . a),(f . b)] in RelIncl A by ; :: thesis: verum
end;
assume that
A16: a in field R and
A17: b in field R and
A18: [(f . a),(f . b)] in RelIncl A ; :: thesis: [a,b] in R
[a,(f . a)] in f by ;
then A19: [a,(f . b)] in f * () by ;
( (f ") . (f . b) = b & f . b in A ) by ;
then [(f . b),b] in g by ;
hence [a,b] in R by ; :: thesis: verum
end;
then f " is_isomorphism_of RelIncl A,R by WELLORD1:39;
then ( R is connected & R is well_founded ) by WELLORD1:43;
then A20: ( R is_connected_in X & R is_well_founded_in X ) by A8;
take R ; :: thesis: ( R well_orders X & order_type_of R = A )
A21: R is_antisymmetric_in X by ;
( R is_reflexive_in X & R is_transitive_in X ) by ;
hence R well_orders X by ; :: thesis:
then A22: R is well-ordering by ;
R, RelIncl A are_isomorphic by A9;
hence order_type_of R = A by ; :: thesis: verum