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 S₁[ Ordinal] means ( $1 c= M & X,$1 are_equipotent );
reconsider m = M as Ordinal ;
assume X c= M ; :: thesis: card X c= M
then ( order_type_of (RelIncl X) c= m & RelIncl X is well-ordering & field (RelIncl X) = X ) by WELLORD2:9, WELLORD2:17, WELLORD2:def 1;
then A1: ex A being Ordinal st S₁[A] by Th22;
consider A being Ordinal such that
A2: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1);
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 A3: B,A are_equipotent ; :: thesis: A c= B
assume A4: not A c= B ; :: thesis: contradiction
then m c= B by A2, A3, WELLORD2:22;
hence contradiction by A2, A4, XBOOLE_1:1; :: thesis: verum

end;

then reconsider A = A as Cardinal ;
card X = A by A2, Def5;
hence card X c= M by A2; :: thesis: verum