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

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

hence
TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
; :: thesis: verum
A1:
[#] X0 = the carrier of X0
;

hence [#] S c= [#] X by PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b_{1} being Element of bool the carrier of S holds

( ( not b_{1} in the topology of S or ex b_{2} being Element of bool the carrier of X st

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

( not b_{2} in the topology of X or not b_{1} = b_{2} /\ ([#] S) ) or b_{1} in the topology of S ) )

let P be Subset of S; :: thesis: ( ( not P in the topology of S or ex b_{1} being Element of bool the carrier of X st

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

( not b_{1} in the topology of X or not P = b_{1} /\ ([#] 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 A1, PRE_TOPC:def 4; :: thesis: ( for b_{1} being Element of bool the carrier of X holds

( not b_{1} in the topology of X or not P = b_{1} /\ ([#] 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 A1, A2, PRE_TOPC:def 4; :: thesis: verum

end;hence [#] S c= [#] X by PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b

( ( not b

( b

( not b

let P be Subset of S; :: thesis: ( ( not P in the topology of S or ex b

( b

( not b

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 A1, PRE_TOPC:def 4; :: thesis: ( for b

( not b

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 A1, A2, PRE_TOPC:def 4; :: thesis: verum