:: deftheorem Def5 defines | PRE_TOPC:def 5 :
for T being TopStruct
for P being Subset of T
for b₃ being strict SubSpace of T holds
( b₃ = T | P iff [#] b₃ = P );