for Y being non empty TopStruct
for y being Point of Y st Sspace y is TopSpace-like holds
( Sspace y is discrete & Sspace y is anti-discrete ) ;