:: deftheorem Def1 defines SubSpace TSP_1:def 1 :
for Y, b₂ being TopStruct holds
( b₂ is SubSpace of Y iff ( the carrier of b₂ c= the carrier of Y & ( for G0 being Subset of b₂ holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b₂ ) ) ) ) );