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: ( 1 in {{} ,1} & not 1 in A ) by TARSKI:def 1, TARSKI:def 2;
then not {{} ,1} \ A is empty by XBOOLE_0:def 5;
then A2: ( A is closed & A is boundary ) by Th25;
then Int A <> A ;
then not A is open by TOPS_1:55;
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 A1, A2, TDLAT_3:17, TDLAT_3:21; :: thesis: verum