let T be non empty T_0 TopSpace; :: thesis: card the carrier of T c= card the topology of T
defpred S₁[ Element of T, set ] means $2 = ([#] T) \ (Cl {$1});
A1: for e being Element of T ex u being Element of the topology of T st S₁[e,u]

proof

let e be Element of T; :: thesis: ex u being Element of the topology of T st S₁[e,u]
reconsider u = ([#] T) \ (Cl {e}) as Element of the topology of T by PRE_TOPC:def 2, PRE_TOPC:def 3;
take u ; :: thesis: S₁[e,u]
thus S₁[e,u] ; :: thesis: verum

end;

consider f being Function of the carrier of T, the topology of T such that
A2: for e being Element of T holds S₁[e,f . e] from FUNCT_2:sch 3(A1);
A3: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A4: ( x1 in dom f & x2 in dom f ) and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of T by A4;
(Cl {y1}) ` = ([#] T) \ (Cl {y1}) by SUBSET_1:def 4
.= f . x2 by A2, A5
.= ([#] T) \ (Cl {y2}) by A2
.= (Cl {y2}) ` by SUBSET_1:def 4 ;
then ( Cl {y2} c= Cl {y1} & Cl {y1} c= Cl {y2} ) by SUBSET_1:12;
hence x1 = x2 by XBOOLE_0:def 10, YELLOW_8:23; :: thesis: verum

end;

( dom f = the carrier of T & rng f c= the topology of T ) by FUNCT_2:def 1;
hence card the carrier of T c= card the topology of T by A3, CARD_1:10; :: thesis: verum