:: deftheorem Def2 defines SubSpace TSP_1:def 2 :
for Y, b₂ being TopStruct holds
( b₂ is SubSpace of Y iff ( the carrier of b₂ c= the carrier of Y & ( for F0 being Subset of b₂ holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b₂ ) ) ) ) );