let T be TopStruct ; :: thesis: for S being SubSpace of TopStruct(# the carrier of T,the topology of T #) holds S is SubSpace of T
let S be SubSpace of TopStruct(# the carrier of T,the topology of T #); :: thesis: S is SubSpace of T
( [#] S c= [#] TopStruct(# the carrier of T,the topology of T #) & ( 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) ) ) ) ) by Def9;
hence ( [#] S c= [#] T & ( 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) ) ) ) ) ; :: according to PRE_TOPC:def 9 :: thesis: verum