let T1, T2 be TopStruct ; :: thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like implies T2 is TopSpace-like )
assume that
A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) and
A2: T1 is TopSpace-like ; :: thesis: T2 is TopSpace-like
thus the carrier of T2 in the topology of T2 by A1, A2, PRE_TOPC:def 1; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b₁ being Element of bool (bool the carrier of T2) holds
( not b₁ c= the topology of T2 or union b₁ in the topology of T2 ) ) & ( for b₁, b₂ being Element of bool the carrier of T2 holds
( not b₁ in the topology of T2 or not b₂ in the topology of T2 or b₁ /\ b₂ in the topology of T2 ) ) )
thus ( ( for b₁ being Element of bool (bool the carrier of T2) holds
( not b₁ c= the topology of T2 or union b₁ in the topology of T2 ) ) & ( for b₁, b₂ being Element of bool the carrier of T2 holds
( not b₁ in the topology of T2 or not b₂ in the topology of T2 or b₁ /\ b₂ in the topology of T2 ) ) ) by A1, A2, PRE_TOPC:def 1; :: thesis: verum