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