set D = {{},1};
set Y = ADTS {{},1};
take
ADTS {{},1}
; ( ADTS {{},1} is anti-discrete & not ADTS {{},1} is discrete & ADTS {{},1} is strict & not ADTS {{},1} is empty )
now not ADTS {{},1} is discrete assume
ADTS {{},1} is
discrete
;
contradictionthen
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;
verum end;
hence
( ADTS {{},1} is anti-discrete & not ADTS {{},1} is discrete & ADTS {{},1} is strict & not ADTS {{},1} is empty )
; verum