set S = TopStruct(# the carrier of T, the topology of T #);
thus ( the carrier of TopStruct(# the carrier of T, the topology of T #) in the topology of TopStruct(# the carrier of T, the topology of T #) & ( for a being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st a c= the topology of TopStruct(# the carrier of T, the topology of T #) holds
union a in the topology of TopStruct(# the carrier of T, the topology of T #) ) & ( for a, b being Subset of TopStruct(# the carrier of T, the topology of T #) st a in the topology of TopStruct(# the carrier of T, the topology of T #) & b in the topology of TopStruct(# the carrier of T, the topology of T #) holds
a /\ b in the topology of TopStruct(# the carrier of T, the topology of T #) ) ) by Def1; :: according to PRE_TOPC:def 1 :: thesis: verum