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

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