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 )
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;
given A being Subset of T such that A3: ( A is dense & A is countable ) ; :: thesis: T is separable
( 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