for X being set holds 1TopSp X = X -DiscreteTop X