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

hereby :: thesis: ( ( 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 ) implies weight TM c= iC )

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

end;

assume 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 ; :: thesis: weight TM c= iC
then density TM c= iC by Lm6;
hence weight TM c= iC by Lm7; :: thesis: verum