set D = {{},1};
set Y = 1TopSp {{},1};
take 1TopSp {{},1} ; :: thesis: ( 1TopSp {{},1} is discrete & not 1TopSp {{},1} is anti-discrete & 1TopSp {{},1} is strict & not 1TopSp {{},1} is empty )

now :: thesis: not 1TopSp {{},1} is anti-discrete

assume 1TopSp {{},1} is anti-discrete ; :: thesis: contradiction
then TopStruct(# the carrier of (1TopSp {{},1}), the topology of (1TopSp {{},1}) #) = TopStruct(# the carrier of (ADTS {{},1}), the topology of (ADTS {{},1}) #) ;
then consider d0 being Element of {{},1} such that
A1: {{},1} = {d0} by Th19;
d0 = {} by A1, ZFMISC_1:4;
hence contradiction by A1, ZFMISC_1:4; :: thesis: verum

end;

hence ( 1TopSp {{},1} is discrete & not 1TopSp {{},1} is anti-discrete & 1TopSp {{},1} is strict & not 1TopSp {{},1} is empty ) ; :: thesis: verum