let T be non empty T_0 TopSpace; :: thesis: card the carrier of T c= card the topology of T

defpred S_{1}[ 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_{1}[e,u]

A2: for e being Element of T holds S_{1}[e,f . e]
from FUNCT_2:sch 3(A1);

A3: f is one-to-one

hence card the carrier of T c= card the topology of T by A3, CARD_1:10; :: thesis: verum

defpred S

A1: for e being Element of T ex u being Element of the topology of T st S

proof

consider f being Function of the carrier of T, the topology of T such that
let e be Element of T; :: thesis: ex u being Element of the topology of T st S_{1}[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_{1}[e,u]

thus S_{1}[e,u]
; :: thesis: verum

end;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

thus S

A2: for e being Element of T holds S

A3: f is one-to-one

proof

( dom f = the carrier of T & rng f c= the topology of T )
by FUNCT_2:def 1;
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;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

hence card the carrier of T c= card the topology of T by A3, CARD_1:10; :: thesis: verum