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

proof

let P be Subset of X; :: thesis: ( P in the topology of X iff ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X) ) )
thus ( P in the topology of X implies ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X) ) ) :: thesis: ( ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X) ) implies P in the topology of X )

proof

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

end;

thus ( ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] X) ) implies P in the topology of X ) by XBOOLE_1:28; :: thesis: verum

end;