let X be set ; :: thesis: for M being Cardinal st X c= M holds
card X c= M
let M be Cardinal; :: thesis: ( X c= M implies card X c= M )
defpred S1[ Ordinal] means ( $1 c= M & X,$1 are_equipotent );
reconsider m = M as Ordinal ;
assume X c= M ; :: thesis: card X c= M
then A1: ( order_type_of (RelIncl X) c= m & RelIncl X is well-ordering ) by WELLORD2:8, WELLORD2:14;
field (RelIncl X) = X by WELLORD2:def 1;
then A2: ex A being Ordinal st S1[A] by A1, Th5;
consider A being Ordinal such that
A3: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
 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 A4: B,A are_equipotent ; :: thesis: A c= B
assume A5: not A c= B ; :: thesis: contradiction
then m c= B by A3, A4, WELLORD2:15;
hence contradiction by A3, A5; :: thesis: verum
end;
then reconsider A = A as Cardinal ;
card X = A by A3, Def2;
hence card X c= M by A3; :: thesis: verum