for Y being non empty TopStruct
for y being Point of Y st Sspace y is proper holds
not Y is trivial ;