set D = {{},1};
reconsider a = {} as Element of {{},1} by TARSKI:def 2;
set Y = STS ({{},1},a);
take
STS ({{},1},a)
; ( not STS ({{},1},a) is anti-discrete & not STS ({{},1},a) is discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty )
reconsider A = {a} as non empty Subset of (STS ({{},1},a)) ;
A1:
not 1 in A
by TARSKI:def 1;
1 in {{},1}
by TARSKI:def 2;
then A2:
not {{},1} \ A is empty
by A1, XBOOLE_0:def 5;
then
A is boundary
by Th21;
then
Int A <> A
;
then A3:
not A is open
by TOPS_1:23;
A is closed
by A2, Th21;
hence
( not STS ({{},1},a) is anti-discrete & not STS ({{},1},a) is discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty )
by A3, TDLAT_3:19; verum