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) by Th44;
hence 1TopSp X = X -DiscreteTop X by A1, ZFMISC_1:40; :: thesis: verum