let S, T be TopStruct ; ( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
thus
( S is SubSpace of T implies S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
( S is SubSpace of TopStruct(# the carrier of T, the topology of T #) implies S is SubSpace of T )proof
assume A1:
S is
SubSpace of
T
;
S is SubSpace of TopStruct(# the carrier of T, the topology of T #)
then
[#] S c= [#] T
by Def4;
hence
[#] S c= [#] TopStruct(# the
carrier of
T, the
topology of
T #)
;
PRE_TOPC:def 4 for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
let P be
Subset of
S;
( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
thus
(
P in the
topology of
S implies ex
Q being
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #) st
(
Q in the
topology of
TopStruct(# the
carrier of
T, the
topology of
T #) &
P = Q /\ ([#] S) ) )
by A1, Def4;
( ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being
Subset of
TopStruct(# the
carrier of
T, the
topology of
T #)
such that A2:
(
Q in the
topology of
TopStruct(# the
carrier of
T, the
topology of
T #) &
P = Q /\ ([#] S) )
;
P in the topology of S
thus
P in the
topology of
S
by A1, A2, Def4;
verum
end;
assume A3:
S is SubSpace of TopStruct(# the carrier of T, the topology of T #)
; S is SubSpace of T
then
[#] S c= [#] TopStruct(# the carrier of T, the topology of T #)
by Def4;
hence
[#] S c= [#] T
; PRE_TOPC:def 4 for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
let P be Subset of S; ( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
thus
( P in the topology of S implies ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
by A3, Def4; ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being Subset of T such that A4:
( Q in the topology of T & P = Q /\ ([#] S) )
; P in the topology of S
thus
P in the topology of S
by A3, A4, Def4; verum