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 :: thesis: not ADTS {{},1} is discrete

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}) #) ;
then consider d0 being Element of {{},1} such that
A2: {{},1} = {d0} by Th19;
d0 = {} by A2, ZFMISC_1:4;
hence contradiction by A2, ZFMISC_1:4; :: 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