let X be infinite set ; :: thesis: card (Fin X) = card X
set FX = Fin X;
deffunc H₁( set ) -> set = proj2 $1;
consider f being Function such that
A1: ( dom f = X * & ( for a being set st a in X * holds
f . a = H₁(a) ) ) from FUNCT_1:sch 3();
Fin X c= rng f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Fin X or a in rng f )
assume a in Fin X ; :: thesis: a in rng f
then A2: ( a c= X & a is finite ) by FINSUB_1:def 5;
then consider p being FinSequence such that
A3: a = rng p by FINSEQ_1:73;
p is FinSequence of X by A2, A3, FINSEQ_1:def 4;
then p in X * by FINSEQ_1:def 11;
then ( f . p in rng f & f . p = proj2 p & proj2 p = a ) by A1, A3, FUNCT_1:def 5;
hence a in rng f ; :: thesis: verum

end;

then card (Fin X) c= card (X * ) by A1, CARD_1:28;
hence card (Fin X) c= card X by CARD_4:87; :: according to XBOOLE_0:def 10 :: thesis: card X c= card (Fin X)
set SX = SmallestPartition X;
SmallestPartition X c= Fin X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in SmallestPartition X or a in Fin X )
assume a in SmallestPartition X ; :: thesis: a in Fin X
then a in { {x} where x is Element of X : verum } by EQREL_1:46;
then ex x being Element of X st a = {x} ;
hence a in Fin X by FINSUB_1:def 5; :: thesis: verum

end;

then card (SmallestPartition X) c= card (Fin X) by CARD_1:27;
hence card X c= card (Fin X) by Th13; :: thesis: verum