let T be TopStruct ; :: thesis: TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
set S = TopStruct(# the carrier of T, the topology of T #);
thus [#] TopStruct(# the carrier of T, the topology of T #) c= [#] T ; :: according to PRE_TOPC:def 4 :: thesis: for b₁ being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) holds
( ( not b₁ in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b₂ being Element of K10( the carrier of T) st
( b₂ in the topology of T & b₁ = b₂ /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b₂ being Element of K10( the carrier of T) holds
( not b₂ in the topology of T or not b₁ = b₂ /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or b₁ in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
let P be Subset of TopStruct(# the carrier of T, the topology of T #); :: thesis: ( ( not P in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b₁ being Element of K10( the carrier of T) st
( b₁ in the topology of T & P = b₁ /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b₁ being Element of K10( the carrier of T) holds
( not b₁ in the topology of T or not P = b₁ /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) ) )

hereby :: thesis: ( for b₁ being Element of K10( the carrier of T) holds
( not b₁ in the topology of T or not P = b₁ /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) )

reconsider Q = P as Subset of T ;
assume A1: P in the topology of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
take Q = Q; :: thesis: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
thus Q in the topology of T by A1; :: thesis: P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #))
thus P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) by XBOOLE_1:28; :: thesis: verum

end;

given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ; :: thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)
thus P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; :: thesis: verum