let X be set ; :: thesis: ex A being Ordinal st X,A are_equipotent
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set Q = R |_2 X;
take A = order_type_of (R |_2 X); :: thesis: X,A are_equipotent
R |_2 X is well-ordering by A1, WELLORD2:16;
then R |_2 X, RelIncl A are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A2: f is_isomorphism_of R |_2 X, RelIncl A by WELLORD1:def 8;
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = X & proj2 f = A )
( dom f = field (R |_2 X) & rng f = field (RelIncl A) ) by A2, WELLORD1:def 7;
hence ( f is one-to-one & proj1 f = X & proj2 f = A ) by A1, A2, WELLORD1:def 7, WELLORD2:16, WELLORD2:def 1; :: thesis: verum