let TM be metrizable TopSpace; :: thesis: for iC being infinite Cardinal holds
( weight TM c= iC iff density TM c= iC )
let iC be infinite Cardinal; :: thesis: ( weight TM c= iC iff density TM c= iC )
consider A being Subset of TM such that
A1: A is dense and
A2: density TM = card A by TOPGEN_1:def 12;

hereby :: thesis: ( density TM c= iC implies weight TM c= iC )

assume weight TM c= iC ; :: thesis: density TM c= iC
then for F being Subset-Family of TM st F is open & not {} in F & ( for A, B being Subset of TM st A in F & B in F & A <> B holds
A misses B ) holds
card F c= iC by Th21;
hence density TM c= iC by Lm6; :: thesis: verum

end;

A3: weight TM c= omega *` (card A) by A1, Th17;
assume density TM c= iC ; :: thesis: weight TM c= iC
then omega *` (card A) c= omega *` iC by A2, CARD_2:90;
then weight TM c= omega *` iC by A3;
hence weight TM c= iC by Lm5; :: thesis: verum