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