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

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