let TM be metrizable TopSpace; :: thesis: for iC being infinite Cardinal st density TM c= iC holds
weight TM c= iC
let iC be infinite Cardinal; :: thesis: ( density TM c= iC implies weight 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;
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