let T be TopStruct ; :: thesis: ( T is finite implies T is second-countable )
assume T is finite ; :: thesis: T is second-countable
then reconsider T' = T as finite TopStruct ;
weight T' is finite by TOPGEN_2:def 4;
then weight T' c= omega ;
hence T is second-countable by WAYBEL23:def 6; :: thesis: verum