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 #) by Def4;
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) ) ) ) ) by Def4; :: according to PRE_TOPC:def 4 :: thesis: verum