let T be TopSpace; :: thesis: ( T is second-countable implies T is Lindelof )
assume A1: T is second-countable ; :: 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 that
A2: F is open and
A3: 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 )

per cases ( T is empty or not T is empty ) ;

suppose A4: T is empty ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )

take F ; :: thesis: ( F c= F & F is Cover of T & F is countable )
F c= {{}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in {{}} )
assume x in F ; :: thesis: x in {{}}
then x = {} by A4;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

hence ( F c= F & F is Cover of T & F is countable ) by A3; :: thesis: verum

end;

suppose not T is empty ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable )

hence ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is countable ) by A1, A2, A3, COMPL_SP:34; :: thesis: verum

end;

end;