:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :
for T being TopStruct holds
( T is finite-weight iff weight T is finite );