let X be TopStruct ; :: thesis: for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
let X0 be SubSpace of X; :: thesis: TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
reconsider S = TopStruct(# the carrier of X0, the topology of X0 #) as TopStruct ;
S is SubSpace of X
proof
A1: [#] X0 = the carrier of X0 ;
hence [#] S c= [#] X by PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b1 being Element of bool the carrier of S holds
( ( not b1 in the topology of S or ex b2 being Element of bool the carrier of X st
( b2 in the topology of X & b1 = b2 /\ ([#] S) ) ) & ( for b2 being Element of bool the carrier of X holds
( not b2 in the topology of X or not b1 = b2 /\ ([#] S) ) or b1 in the topology of S ) )

let P be Subset of S; :: thesis: ( ( not P in the topology of S or ex b1 being Element of bool the carrier of X st
( b1 in the topology of X & P = b1 /\ ([#] S) ) ) & ( for b1 being Element of bool the carrier of X holds
( not b1 in the topology of X or not P = b1 /\ ([#] S) ) or P in the topology of S ) )

thus ( P in the topology of S implies ex Q being Subset of X st
( Q in the topology of X & P = Q /\ ([#] S) ) ) by ; :: thesis: ( for b1 being Element of bool the carrier of X holds
( not b1 in the topology of X or not P = b1 /\ ([#] S) ) or P in the topology of S )

given Q being Subset of X such that A2: ( Q in the topology of X & P = Q /\ ([#] S) ) ; :: thesis: P in the topology of S
thus P in the topology of S by ; :: thesis: verum
end;
hence TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X ; :: thesis: verum