let TM be metrizable TopSpace; :: thesis: for B being Basis of TM st TM is Lindelof holds
ex B9 being Basis of TM st
( B9 c= B & B9 is countable )
let B be Basis of TM; :: thesis: ( TM is Lindelof implies ex B9 being Basis of TM st
( B9 c= B & B9 is countable ) )
assume TM is Lindelof ; :: thesis: ex B9 being Basis of TM st
( B9 c= B & B9 is countable )
then for F being Subset-Family of TM st F is open & F is Cover of TM holds
ex G being Subset-Family of TM st
( G c= F & G is Cover of TM & card G c= omega ) by Lm8;
then consider underB being Basis of TM such that
A1: ( underB c= B & card underB c= omega ) by Th23;
take underB ; :: thesis: ( underB c= B & underB is countable )
thus ( underB c= B & underB is countable ) by A1; :: thesis: verum