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 A2, A3, FUNCT_2:2;
reconsider g = f " as Function of A,X by A1, A3, FUNCT_2:25;
A4: dom g = A by A1, A3, FUNCT_1:33;
reconsider f9 = f as one-to-one Function by A1;
A5: dom (RelIncl A) = A by ORDERS_1:14;
rng (RelIncl A) = A by ORDERS_1:14;
then A6: rng (f * (RelIncl A)) = A by A3, A5, RELAT_1:28;
set R = (f * (RelIncl A)) * g;
dom (f * (RelIncl A)) = X by A2, A3, A5, RELAT_1:27;
then A7: dom ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:27;
rng g = X by A1, A2, FUNCT_1:33;
then rng ((f * (RelIncl A)) * g) = X by A4, A6, RELAT_1:28;
then A8: field ((f * (RelIncl A)) * g) = X \/ X by A7, RELAT_1:def 6
.= X ;
reconsider R = (f * (RelIncl A)) * g as Relation of X ;
(f9 * (RelIncl A)) * (f9 ") is_reflexive_in X by A8, RELAT_2:def 9;
then reconsider R = R as Order of X by A7, PARTFUN1:def 2;
A9: f is_isomorphism_of R, RelIncl A

proof

thus ( dom f = field R & rng f = field (RelIncl A) & f is one-to-one ) by A1, A2, A3, A8, WELLORD2:def 1; :: according to WELLORD1:def 7 :: thesis: for b₁, b₂ being object holds
( ( not [b₁,b₂] in R or ( b₁ in field R & b₂ in field R & [(f . b₁),(f . b₂)] in RelIncl A ) ) & ( not b₁ in field R or not b₂ in field R or not [(f . b₁),(f . b₂)] in RelIncl A or [b₁,b₂] 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 * (RelIncl A) and
A12: [x,b] in g by A10, RELAT_1:def 8;
A13: ( b = g . x & x in dom g ) by A12, FUNCT_1:1;
consider y being object such that
A14: [a,y] in f and
A15: [y,x] in RelIncl A by A11, RELAT_1:def 8;
y = f . a by A14, FUNCT_1:1;
hence [(f . a),(f . b)] in RelIncl A by A1, A3, A15, A13, FUNCT_1:35; :: 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 A2, A8, A16, FUNCT_1:1;
then A19: [a,(f . b)] in f * (RelIncl A) by A18, RELAT_1:def 8;
( (f ") . (f . b) = b & f . b in A ) by A1, A2, A3, A8, A17, FUNCT_1:34, FUNCT_1:def 3;
then [(f . b),b] in g by A4, FUNCT_1:1;
hence [a,b] in R by A19, RELAT_1:def 8; :: 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 A8, RELAT_2:def 12;
( R is_reflexive_in X & R is_transitive_in X ) by A8, RELAT_2:def 9, RELAT_2:def 16;
hence R well_orders X by A21, A20; :: thesis: order_type_of R = A
then A22: R is well-ordering by A8, WELLORD1:4;
R, RelIncl A are_isomorphic by A9;
hence order_type_of R = A by A22, WELLORD2:def 2; :: thesis: verum