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_{1} being Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #) holds

( ( not b_{1} in the topology of TopStruct(# the carrier of T, the topology of T #) or ex b_{2} being Element of bool the carrier of T st

( b_{2} in the topology of T & b_{1} = b_{2} /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b_{2} being Element of bool the carrier of T holds

( not b_{2} in the topology of T or not b_{1} = b_{2} /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or b_{1} 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_{1} being Element of bool the carrier of T st

( b_{1} in the topology of T & P = b_{1} /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ) & ( for b_{1} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not P = b_{1} /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) or 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

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

( ( not b

( b

( not b

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

( b

( not b

hereby :: thesis: ( for b_{1} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not P = b_{1} /\ ([#] 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 #)) )
; :: thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)( not b

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;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

thus P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; :: thesis: verum