let TM be metrizable TopSpace; :: thesis: for iC being infinite Cardinal holds
( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds
card Am c= iC )
let iC be infinite Cardinal; :: thesis: ( weight TM c= iC iff for Am being Subset of TM st Am is discrete holds
card Am c= iC )

hereby :: thesis: ( ( for Am being Subset of TM st Am is discrete holds
card Am c= iC ) implies weight TM c= iC )

assume weight TM c= iC ; :: thesis: for A being Subset of TM st A is discrete holds
card A c= iC
then for A being Subset of TM st A is closed & A is discrete holds
card A c= iC by Th19;
hence for A being Subset of TM st A is discrete holds
card A c= iC by Th14; :: thesis: verum

end;

assume for A being Subset of TM st A is discrete holds
card A c= iC ; :: thesis: weight 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 Th15;
then density TM c= iC by Lm6;
hence weight TM c= iC by Lm7; :: thesis: verum