let T be TopStruct ; :: thesis: ( T is finite implies T is finite-weight )
assume A1: the carrier of T is finite ; :: according to STRUCT_0:def 11 :: thesis: T is finite-weight
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence weight T is finite by A1; :: according to TOPGEN_2:def 4 :: thesis: verum