let T be non empty discrete TopSpace; :: thesis: ( T is separable iff card ([#] T) c= omega )

then T is countable by TOPGEN_1:2;

hence T is separable ; :: thesis: verum

hereby :: thesis: ( card ([#] T) c= omega implies T is separable )

assume
card ([#] T) c= omega
; :: thesis: 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;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

then T is countable by TOPGEN_1:2;

hence T is separable ; :: thesis: verum