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