let T be non empty TopSpace; :: thesis: ( T is second-countable implies ex B being Basis of T st B is countable )
assume A1: T is second-countable ; :: thesis: ex B being Basis of T st B is countable
consider B being Basis of T;
consider B1 being Basis of T such that
A2: ( B1 c= B & card B1 = weight T ) by TOPGEN_2:20;
card B1 c= omega by A1, A2, WAYBEL23:def 6;
then card (card B1) c= card omega by CARD_1:27;
then B1 is countable by WAYBEL12:2;
hence ex B being Basis of T st B is countable ; :: thesis: verum