:: deftheorem Def2 defines Sspace TEX_2:def 2 :
for Y being non empty TopStruct
for y being Point of Y
for b₃ being non empty strict SubSpace of Y holds
( b₃ = Sspace y iff the carrier of b₃ = {y} );