let iC be infinite Cardinal; :: thesis:
let TM be metrizable TopSpace; :: thesis:
assume A1: for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC ; :: thesis:
let Am be Subset of TM; :: thesis:
assume A2: Am is discrete ; :: thesis:

per cases ;

suppose Am is empty ; :: thesis:

hence card Am c= iC ; :: thesis:

end;

suppose A3: not Am is empty ; :: thesis:

then reconsider Tm = TM as non empty metrizable TopSpace ;
Am c= Cl Am by PRE_TOPC:48;
then reconsider ClA = Cl Am as non empty closed Subset of Tm by A3;
set TA = TM | (Cl Am);
set TA = Tm | ClA;
reconsider A' = Am as open Subset of (Tm | ClA) by A2, Th13;
consider F being countable closed Subset-Family of (Tm | ClA) such that
A4: A' = union F by TOPGEN_4:def 6;
consider f being Function of NAT ,F such that
A5: rng f = F by A3, A4, CARD_3:146, ZFMISC_1:2;
A6: for x being set st x in dom f holds
card (f . x) c= iC

let x be set ; :: thesis:
assume x in dom f ; :: thesis:
then A7: f . x in rng f by FUNCT_1:def 5;
then reconsider fx = f . x as Subset of (Tm | ClA) by A5;
A8: f . x c= Am by A4, A7, ZFMISC_1:92;
then reconsider Fx = f . x as Subset of TM by XBOOLE_1:1;
( [#] (Tm | ClA) = ClA & fx is closed ) by A7, PRE_TOPC:def 10, TOPS_2:def 2;
then Fx is closed by TSEP_1:8;
hence card (f . x) c= iC by A1, A2, A8, TEX_2:28; :: thesis:

end;

card (dom f) = omega by A3, A4, CARD_1:84, FUNCT_2:def 1, ZFMISC_1:2;
then card (Union f) c= omega *` iC by A6, CARD_3:132;
hence card Am c= iC by A4, A5, Lm6; :: thesis:

end;