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 A50: card ([#] T) c= omega by CARD_3:def 14;
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
A51: 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
A52: ( G c= F & G is Cover of T ) and
A53: card G c= card ([#] T) by A51, Th16;
take G ; :: thesis: ( G c= F & G is Cover of T & G is countable )
card G c= omega by A50, A53, XBOOLE_1:1;
hence ( G c= F & G is Cover of T & G is countable ) by A52, CARD_3:def 14; :: thesis: verum