let T be TopStruct ; :: thesis: ( TopStruct(# the carrier of T, the topology of T #) is TopSpace-like implies T is TopSpace-like )
set S = TopStruct(# the carrier of T, the topology of T #);
assume ( 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 #) ) ) ; :: according to PRE_TOPC:def 1 :: thesis: T is TopSpace-like
hence ( the carrier of T in the topology of T & ( for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T ) & ( for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T ) ) ; :: according to PRE_TOPC:def 1 :: thesis: verum