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