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

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