let TM be metrizable TopSpace; :: thesis: ( TM is Lindelof iff TM is separable )

hereby :: thesis: ( TM is separable implies TM is Lindelof )

assume TM is Lindelof ; :: thesis: TM is separable
then weight TM c= omega by WAYBEL23:def 6;
then density TM c= omega by Th22;
hence TM is separable by TOPGEN_1:def 13; :: thesis: verum

end;

assume TM is separable ; :: thesis: TM is Lindelof
then density TM c= omega by TOPGEN_1:def 13;
then weight TM c= omega by Th22;
then TM is second-countable by WAYBEL23:def 6;
hence TM is Lindelof by Lm9; :: thesis: verum