:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :
for IT being TopStruct holds
( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) ) );