let T be TopSpace; :: thesis: ( T is Lindelof iff for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= omega ) )

hereby :: thesis: ( ( for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= omega ) ) implies T is Lindelof )

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

end;

assume A4: for F being Subset-Family of T st F is open & F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= omega ) ; :: thesis: T is Lindelof
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 A5: ( F is open & 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
A6: ( G c= F & G is Cover of T ) and
A7: card G c= omega by A4, A5;
G is countable by A7, CARD_3:def 15;
hence ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) by A6; :: thesis: verum