let T be non empty TopSpace; :: thesis: ( T is second-countable implies T is separable )

assume T is second-countable ; :: thesis: T is separable

then A1: weight T c= omega by WAYBEL23:def 6;

density T c= weight T by Th5;

then density T c= omega by A1;

hence T is separable by TOPGEN_1:def 13; :: thesis: verum

assume T is second-countable ; :: thesis: T is separable

then A1: weight T c= omega by WAYBEL23:def 6;

density T c= weight T by Th5;

then density T c= omega by A1;

hence T is separable by TOPGEN_1:def 13; :: thesis: verum