set D = {{},1};
reconsider a = {} as Element of {{},1} by TARSKI:def 2;
set Y = STS ({{},1},a);
take STS ({{},1},a) ; :: thesis: ( 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;
A2: 1 in {{},1} by TARSKI:def 2;
then A3: not {{},1} \ A is empty by A1, XBOOLE_0:def 5;
then A is boundary by Th25;
then Int A <> A ;
then A4: not A is open by TOPS_1:55;
A is closed by A3, Th25;
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 A2, A1, A4, TDLAT_3:17, TDLAT_3:21; :: thesis: verum