let T be TopSpace; :: thesis: ( T is countable implies T is Lindelof )
assume T is countable ; :: thesis: T is Lindelof
then [#] T is countable by ORDERS_4:def 2;
then A51: card ([#] T) c= omega ;
let F be Subset-Family of T; :: according to METRIZTS:def 2 :: thesis: ( F is open & F is Cover of T implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) )
assume that
F is open and
A52: F is Cover of T ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )
consider G being Subset-Family of T such that
A53: ( G c= F & G is Cover of T ) and
A54: card G c= card ([#] T) by A52, Th16;
take G ; :: thesis: ( G c= F & G is Cover of T & G is countable )
card G c= omega by A51, A54;
hence ( G c= F & G is Cover of T & G is countable ) by A53; :: thesis: verum