let T be TopStruct ; 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
; PRE_TOPC:def 4 for b1 being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds
( ( not b1 in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b2 being Element of bool the carrier of T st
( b2 in the topology of T & b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b2 being Element of bool the carrier of T holds
( not b2 in the topology of T or not b1 = b2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or b1 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 #); ( ( not P in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b1 being Element of bool the carrier of T st
( b1 in the topology of T & P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b1 being Element of bool the carrier of T holds
( not b1 in the topology of T or not P = b1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or P in the topology of TopStruct(# the carrier of T, the topology of T #) ) )
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 #)) )
; 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; verum