for X being set
for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)