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