let S, T be TopStruct ; :: thesis: ( 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 #) )
:: thesis: ( S is SubSpace of TopStruct(# the carrier of T,the topology of T #) implies S is SubSpace of T )proof
assume Z:
S is
SubSpace of
T
;
:: thesis: S is SubSpace of TopStruct(# the carrier of T,the topology of T #)
then
[#] S c= [#] T
by Def9;
hence
[#] S c= [#] TopStruct(# the
carrier of
T,the
topology of
T #)
;
:: according to PRE_TOPC:def 9 :: thesis: 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;
:: thesis: ( 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 Z, Def9;
:: thesis: ( 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 G:
(
Q in the
topology of
TopStruct(# the
carrier of
T,the
topology of
T #) &
P = Q /\ ([#] S) )
;
:: thesis: P in the topology of S
reconsider Q =
Q as
Subset of
T ;
Q in the
topology of
T
by G;
hence
P in the
topology of
S
by G, Z, Def9;
:: thesis: verum
end;
assume Z:
S is SubSpace of TopStruct(# the carrier of T,the topology of T #)
; :: thesis: S is SubSpace of T
then
[#] S c= [#] TopStruct(# the carrier of T,the topology of T #)
by Def9;
hence
[#] S c= [#] T
; :: according to PRE_TOPC:def 9 :: thesis: 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; :: thesis: ( 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 Z, Def9; :: thesis: ( 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 G:
( Q in the topology of T & P = Q /\ ([#] S) )
; :: thesis: P in the topology of S
reconsider Q = Q as Subset of T ;
Q in the topology of T
by G;
hence
P in the topology of S
by G, Z, Def9; :: thesis: verum