for Y being non empty TopStruct
for y being Point of Y holds
( Sspace y is proper iff {y} is proper )