theorem Th23: :: METRIZTS:23
for TM being metrizable TopSpace
for iC being infinite Cardinal
for B being Basis of TM st ( 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 ) ) holds
ex underB being Basis of TM st
( underB c= B & card underB c= iC )