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 ( 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 )
then consider G being Subset-Family of T such that
A2: ( G c= F & G is Cover of T & G is countable ) by A1;
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 A2; :: thesis: verum

end;

assume A3: 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 ( 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 )
then consider G being Subset-Family of T such that
A4: ( G c= F & G is Cover of T ) and
A5: card G c= omega by A3;
G is countable by A5;
hence ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) by A4; :: thesis: verum