:: deftheorem Def4 defines SubSpace PRE_TOPC:def 4 :
for T, b₂ being TopStruct holds
( b₂ is SubSpace of T iff ( [#] b₂ c= [#] T & ( for P being Subset of b₂ holds
( P in the topology of b₂ iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b₂) ) ) ) ) );