let T be countable TopSpace; :: thesis: T is separable
( card ([#] T) c= omega & density T c= card ([#] T) ) by Def12, CARD_3:def 14;
then density T c= omega ;
hence T is separable ; :: thesis: verum