let T be non empty discrete TopSpace; :: thesis: ( T is separable iff T is countable )
( T is separable iff card ([#] T) c= omega ) by Th10;
hence ( T is separable iff T is countable ) by TOPGEN_1:2; :: thesis: verum