theorem :: TOPGEN_3:45
for X being set holds ADTS X = {} -DiscreteTop X