let X be TopStruct ; 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; TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
set S = TopStruct(# the carrier of X0, the topology of X0 #);
TopStruct(# the carrier of X0, the topology of X0 #) is SubSpace of X
proof
A1:
[#] X0 = the
carrier of
X0
;
hence
[#] TopStruct(# the
carrier of
X0, the
topology of
X0 #)
c= [#] X
by PRE_TOPC:def 4;
PRE_TOPC:def 4 for b1 being Element of K10( the carrier of TopStruct(# the carrier of X0, the topology of X0 #)) holds
( ( not b1 in the topology of TopStruct(# the carrier of X0, the topology of X0 #) or ex b2 being Element of K10( the carrier of X) st
( b2 in the topology of X & b1 = b2 /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) ) & ( for b2 being Element of K10( the carrier of X) holds
( not b2 in the topology of X or not b1 = b2 /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) or b1 in the topology of TopStruct(# the carrier of X0, the topology of X0 #) ) )
let P be
Subset of
TopStruct(# the
carrier of
X0, the
topology of
X0 #);
( ( not P in the topology of TopStruct(# the carrier of X0, the topology of X0 #) or ex b1 being Element of K10( the carrier of X) st
( b1 in the topology of X & P = b1 /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) ) & ( for b1 being Element of K10( the carrier of X) holds
( not b1 in the topology of X or not P = b1 /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) or P in the topology of TopStruct(# the carrier of X0, the topology of X0 #) ) )
thus
(
P in the
topology of
TopStruct(# the
carrier of
X0, the
topology of
X0 #) implies ex
Q being
Subset of
X st
(
Q in the
topology of
X &
P = Q /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) )
by A1, PRE_TOPC:def 4;
( for b1 being Element of K10( the carrier of X) holds
( not b1 in the topology of X or not P = b1 /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) ) or P in the topology of TopStruct(# the carrier of X0, the topology of X0 #) )
given Q being
Subset of
X such that A2:
(
Q in the
topology of
X &
P = Q /\ ([#] TopStruct(# the carrier of X0, the topology of X0 #)) )
;
P in the topology of TopStruct(# the carrier of X0, the topology of X0 #)
thus
P in the
topology of
TopStruct(# the
carrier of
X0, the
topology of
X0 #)
by A1, A2, PRE_TOPC:def 4;
verum
end;
hence
TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
; verum