theorem :: METRIZTS:24

for TM being metrizable TopSpace
for B being Basis of TM st TM is Lindelof holds
ex B9 being Basis of TM st
( B9 c= B & B9 is countable )