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

now

assume ADTS {{} ,1} is discrete ; :: thesis: contradiction
then TopStruct(# the carrier of (ADTS {{} ,1}),the topology of (ADTS {{} ,1}) #) = TopStruct(# the carrier of (1TopSp {{} ,1}),the topology of (1TopSp {{} ,1}) #) by TDLAT_3:def 1;
then consider d0 being Element of {{} ,1} such that
A2: {{} ,1} = {d0} by Th23;
d0 = {} by A2, ZFMISC_1:8;
hence contradiction by A2, ZFMISC_1:8; :: thesis: verum

end;

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