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 closed & 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 closed & Am is discrete holds
card Am c= iC )

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

assume weight TM c= iC ; :: thesis: for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC
then for Fm being Subset-Family of TM st Fm is open & Fm is Cover of TM holds
ex Gm being Subset-Family of TM st
( Gm c= Fm & Gm is Cover of TM & card Gm c= iC ) by Th18;
hence for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC by Th13; :: thesis: verum

end;

assume for Am being Subset of TM st Am is closed & Am is discrete holds
card Am c= iC ; :: thesis: weight TM c= iC
then for Am being Subset of TM st Am is discrete holds
card Am c= iC by Th14;
then for Fm being Subset-Family of TM st Fm is open & not {} in Fm & ( for Am, Bm being Subset of TM st Am in Fm & Bm in Fm & Am <> Bm holds
Am misses Bm ) holds
card Fm c= iC by Th15;
then density TM c= iC by Lm6;
hence weight TM c= iC by Lm7; :: thesis: verum