let T be non empty TopSpace; :: thesis: ( T is second-countable implies ex B being Basis of T st B is countable )
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
assume T is second-countable ; :: thesis: ex B being Basis of T st B is countable
then card B1 c= omega by A1, WAYBEL23:def 6;
then card (card B1) c= card omega ;
then B1 is countable ;
hence ex B being Basis of T st B is countable ; :: thesis: verum