let T be TopSpace; :: thesis: ( T is Lindelof iff 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 ) )

hereby :: thesis: ( ( 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 ) ) implies T is Lindelof )

assume A1: T is Lindelof ; :: thesis: 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 )
let F be Subset-Family of ; :: thesis: ( F is open & F is Cover of implies ex G being Subset-Family of st
( G c= F & G is Cover of & card G c= omega ) )
assume ( F is open & F is Cover of ) ; :: thesis: ex G being Subset-Family of st
( G c= F & G is Cover of & card G c= omega )
then consider G being Subset-Family of such that
A2: ( G c= F & G is Cover of & G is countable ) by A1, Def2;
take G = G; :: thesis: ( G c= F & G is Cover of & card G c= omega )
thus ( G c= F & G is Cover of & card G c= omega ) by A2, CARD_3:def 15; :: thesis: verum

end;

assume A3: 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 ) ; :: thesis: T is Lindelof
let F be Subset-Family of ; :: according to METRIZTS:def 2 :: thesis: ( F is open & F is Cover of implies ex G being Subset-Family of st
( G c= F & G is Cover of & G is countable ) )
assume ( F is open & F is Cover of ) ; :: thesis: ex G being Subset-Family of st
( G c= F & G is Cover of & G is countable )
then consider G being Subset-Family of such that
A4: ( G c= F & G is Cover of ) and
A5: card G c= omega by A3;
G is countable by A5, CARD_3:def 15;
hence ex G being Subset-Family of st
( G c= F & G is Cover of & G is countable ) by A4; :: thesis: verum