for Y being anti-discrete TopStruct
for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y