theorem :: TOPGEN_3:46

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