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