reconsider O = bool {{} } as Subset-Family of {{} } ;
reconsider T = TopStruct(# {{} },O #) as non empty discrete TopStruct by TDLAT_3:def 1;
take T ; :: thesis: ( T is finite & not T is empty )
thus ( T is finite & not T is empty ) ; :: thesis: verum