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:18;
then reconsider ClA = Cl Am as non empty closed Subset of Tm by A3;
set TA = Tm | ClA;
reconsider A9 = Am as open Subset of (Tm | ClA) by A2, Th12;
consider F being countable closed Subset-Family of (Tm | ClA) such that
A4: A9 = union F by TOPGEN_4:def 6;
consider f being sequence of F such that
A5: rng f = F by A3, A4, CARD_3:96, ZFMISC_1:2;
A6: for x being object st x in dom f holds
card (f . x) c= iC

proof

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

end;

card (dom f) = omega by A3, A4, CARD_1:47, FUNCT_2:def 1, ZFMISC_1:2;
then card (Union f) c= omega *` iC by A6, CARD_2:86;
hence card Am c= iC by A4, A5, Lm5; :: thesis:

end;

end;