let X be TopStruct ; :: thesis: for X1, X2 being TopSpace st X1 = TopStruct(# the carrier of X2, the topology of X2 #) holds
( X1 is SubSpace of X iff X2 is SubSpace of X )
let X1, X2 be TopSpace; :: thesis: ( X1 = TopStruct(# the carrier of X2, the topology of X2 #) implies ( X1 is SubSpace of X iff X2 is SubSpace of X ) )
assume A1: X1 = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: ( X1 is SubSpace of X iff X2 is SubSpace of X )
thus ( X1 is SubSpace of X implies X2 is SubSpace of X ) :: thesis: ( X2 is SubSpace of X implies X1 is SubSpace of X )

proof

A2: [#] X1 = the carrier of X1 ;
assume A3: X1 is SubSpace of X ; :: thesis: X2 is SubSpace of X
hence [#] X2 c= [#] X by A1, A2, PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b₁ being Element of bool the carrier of X2 holds
( ( not b₁ in the topology of X2 or ex b₂ being Element of bool the carrier of X st
( b₂ in the topology of X & b₁ = b₂ /\ ([#] X2) ) ) & ( for b₂ being Element of bool the carrier of X holds
( not b₂ in the topology of X or not b₁ = b₂ /\ ([#] X2) ) or b₁ in the topology of X2 ) )
let P be Subset of X2; :: thesis: ( ( not P in the topology of X2 or ex b₁ being Element of bool the carrier of X st
( b₁ in the topology of X & P = b₁ /\ ([#] X2) ) ) & ( for b₁ being Element of bool the carrier of X holds
( not b₁ in the topology of X or not P = b₁ /\ ([#] X2) ) or P in the topology of X2 ) )
thus ( P in the topology of X2 implies ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X2) ) ) by A1, A3, A2, PRE_TOPC:def 4; :: thesis: ( for b₁ being Element of bool the carrier of X holds
( not b₁ in the topology of X or not P = b₁ /\ ([#] X2) ) or P in the topology of X2 )
given Q being Subset of X such that A4: ( Q in the topology of X & P = Q /\ ([#] X2) ) ; :: thesis: P in the topology of X2
thus P in the topology of X2 by A1, A3, A2, A4, PRE_TOPC:def 4; :: thesis: verum

end;

thus ( X2 is SubSpace of X implies X1 is SubSpace of X ) by A1, Th6; :: thesis: verum