let TM be metrizable TopSpace; :: thesis: ( TM is Lindelof iff TM is second-countable )

hereby :: thesis: ( TM is second-countable implies TM is Lindelof )

assume TM is Lindelof ; :: thesis: TM is second-countable
then for F being Subset-Family of TM st F is open & F is Cover of TM holds
ex G being Subset-Family of TM st
( G c= F & G is Cover of TM & card G c= omega ) by Lm8;
then weight TM c= omega by Th18;
hence TM is second-countable by WAYBEL23:def 6; :: thesis: verum

end;

assume TM is second-countable ; :: thesis: TM is Lindelof
then weight TM c= omega by WAYBEL23:def 6;
then for F being Subset-Family of TM st F is open & F is Cover of TM holds
ex G being Subset-Family of TM st
( G c= F & G is Cover of TM & card G c= omega ) by Th18;
hence TM is Lindelof by Lm8; :: thesis: verum