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: contradictionthen
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 = {} &
d0 = 1 )
by A2, ZFMISC_1:8;
hence
contradiction
;
:: 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