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 by XBOOLE_1:1;
hence T is separable by Def13; :: thesis: verum