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

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}) #) by TDLAT_3:def 2;
then consider d0 being Element of {{},1} such that
A1: {{},1} = {d0} by Th23;
d0 = {} by A1, ZFMISC_1:8;
hence contradiction by A1, ZFMISC_1:8; :: 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