for Y being 1 -element TopStruct st not the topology of Y is empty & Y is almost_discrete holds
Y is TopSpace-like