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