let T be non empty discrete TopSpace; :: thesis: ( T is separable iff card ([#] T) c= omega )
hereby :: thesis: ( card ([#] T) c= omega implies T is separable )
assume T is separable ; :: thesis: card ([#] T) c= omega
then A1: density T c= omega by TOPGEN_1:def 13;
ex A being Subset of T st
( A is dense & density T = card A ) by TOPGEN_1:def 12;
hence card ([#] T) c= omega by A1, TOPS_3:19; :: thesis: verum
end;
assume card ([#] T) c= omega ; :: thesis: T is separable
then T is countable by TOPGEN_1:2;
hence T is separable ; :: thesis: verum