defpred S1[ Ordinal] means X,$1 are_equipotent ;
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set Q = R |_2 X;
set A = order_type_of (R |_2 X);
R |_2 X is well-ordering by A1, WELLORD2:16;
then R |_2 X, RelIncl (order_type_of (R |_2 X)) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A2: f is_isomorphism_of R |_2 X, RelIncl (order_type_of (R |_2 X)) by WELLORD1:def 8;
X, order_type_of (R |_2 X) are_equipotent
proof
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = order_type_of (R |_2 X) )
( dom f = field (R |_2 X) & rng f = field (RelIncl (order_type_of (R |_2 X))) ) by A2, WELLORD1:def 7;
hence ( f is one-to-one & dom f = X & rng f = order_type_of (R |_2 X) ) by A1, A2, WELLORD1:def 7, WELLORD2:16, WELLORD2:def 1; :: thesis: verum
end;
then A3: ex A being Ordinal st S1[A] ;
consider A being Ordinal such that
A4: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
 A is cardinal
proof
take A ; :: according to CARD_1:def 1 :: thesis: ( A = A & ( for A being Ordinal st A,A are_equipotent holds
A c= A ) )
thus A = A ; :: thesis: for A being Ordinal st A,A are_equipotent holds
A c= A
let B be Ordinal; :: thesis: ( B,A are_equipotent implies A c= B )
assume B,A are_equipotent ; :: thesis: A c= B
hence A c= B by A4, WELLORD2:15; :: thesis: verum
end;
then reconsider M = A as Cardinal ;
take M ; :: thesis: X,M are_equipotent
thus X,M are_equipotent by A4; :: thesis: verum