let X be set ; :: thesis: 1TopSp X = X -DiscreteTop X
set T = X -DiscreteTop X;
A1: the carrier of (X -DiscreteTop X) = X by Def8;
X c= X ;
then ( the topology of (X -DiscreteTop X) = {X} \/ (bool X) & X in bool X ) by Th44;
hence 1TopSp X = X -DiscreteTop X by A1, ZFMISC_1:46; :: thesis: verum