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:26;
set Q = R |_2 X;
A2: ( field (R |_2 X) = X & R |_2 X is well-ordering ) by A1, WELLORD2:25;
take A = order_type_of (R |_2 X); :: thesis: X,A are_equipotent
R |_2 X, RelIncl A are_isomorphic by A2, WELLORD2:def 2;
then consider f being Function such that
A3: f is_isomorphism_of R |_2 X, RelIncl A by WELLORD1:def 8;
A4: ( dom f = field (R |_2 X) & rng f = field (RelIncl A) & f is one-to-one & ( for a, b being set holds
( [a,b] in R |_2 X iff ( a in field (R |_2 X) & b in field (R |_2 X) & [(f . a),(f . b)] in RelIncl A ) ) ) ) by A3, WELLORD1:def 7;
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = A )
thus ( f is one-to-one & dom f = X & rng f = A ) by A1, A4, WELLORD2:25, WELLORD2:def 1; :: thesis: verum