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