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

( A is dense & A is countable ) )

( density T c= card A & card A c= omega ) by A3, TOPGEN_1:def 12;

then density T c= omega ;

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

( 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 )

given A being Subset of T such that A3:
( A is dense & A is countable )
; :: thesis: T is separable ( A is dense & A is countable ) implies T is separable )

consider A being Subset of T such that

A1: A is dense and

A2: density T = card A by TOPGEN_1:def 12;

assume T is separable ; :: thesis: ex A being Subset of T st

( A is dense & A is countable )

then density T c= omega by TOPGEN_1:def 13;

then A is countable by A2;

hence ex A being Subset of T st

( A is dense & A is countable ) by A1; :: thesis: verum

end;A1: A is dense and

A2: density T = card A by TOPGEN_1:def 12;

assume T is separable ; :: thesis: ex A being Subset of T st

( A is dense & A is countable )

then density T c= omega by TOPGEN_1:def 13;

then A is countable by A2;

hence ex A being Subset of T st

( A is dense & A is countable ) by A1; :: thesis: verum

( density T c= card A & card A c= omega ) by A3, TOPGEN_1:def 12;

then density T c= omega ;

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