consider A being infinite set ;
reconsider O = bool A as Subset-Family of A ;
reconsider T = TopStruct(# A,O #) as non empty discrete TopStruct by TDLAT_3:def 1;
take T ; :: thesis: not T is finite-weight
weight T = card the carrier of T by Th15;
hence not weight T is finite ; :: according to TOPGEN_2:def 4 :: thesis: verum