let TM be metrizable TopSpace; :: thesis: for B being Basis of TM st TM is Lindelof holds
ex B' being Basis of TM st
( B' c= B & B' is countable )
let B be Basis of TM; :: thesis: ( TM is Lindelof implies ex B' being Basis of TM st
( B' c= B & B' is countable ) )
assume TM is Lindelof ; :: thesis: ex B' being Basis of TM st
( B' c= B & B' is countable )
then for F being Subset-Family of st F is open & F is Cover of holds
ex G being Subset-Family of st
( G c= F & G is Cover of & 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, CARD_3:def 15; :: thesis: verum