let T be non empty TopSpace; :: thesis: ( T is separable iff ex A being Subset of T st
( A is dense & A is countable ) )

hereby :: thesis: ( ex A being Subset of T st
( A is dense & A is countable ) implies T is separable )

assume T is separable ; :: thesis: ex A being Subset of T st
( A is dense & A is countable )
then A1: density T c= omega by TOPGEN_1:def 13;
consider A being Subset of T such that
A2: ( A is dense & density T = card A ) by TOPGEN_1:def 12;
A is countable by A1, A2, CARD_3:def 15;
hence ex A being Subset of T st
( A is dense & A is countable ) by A2; :: thesis: verum

end;

given A being Subset of T such that A3: ( A is dense & A is countable ) ; :: thesis: T is separable
A4: density T c= card A by A3, TOPGEN_1:def 12;
card A c= omega by A3, CARD_3:def 15;
then density T c= omega by A4, XBOOLE_1:1;
hence T is separable by TOPGEN_1:def 13; :: thesis: verum