A1: ( {{} ,{0 }} = bool {0 } & bool {0 } c= bool {0 } ) by ZFMISC_1:30;
0 in {0 } by TARSKI:def 1;
then reconsider r = {[0 ,0 ]} as Relation of {0 } by RELSET_1:8;
reconsider C = bool {0 } as Subset-Family of {0 } ;
reconsider A = TopRelStr(# {0 },r,C #) as non empty trivial finite discrete reflexive TopRelStr by A1, Lm4;
reconsider A = A as TopLattice ;
take A ; :: thesis: ( A is strict & not A is empty & A is trivial & A is discrete & A is finite & A is compact & A is T_2 )
thus ( A is strict & not A is empty & A is trivial & A is discrete & A is finite ) ; :: thesis: ( A is compact & A is T_2 )
thus A is compact ; :: thesis: A is T_2
let p, q be Point of A; :: according to PRE_TOPC:def 16 :: thesis: ( p = q or ex b₁, b₂ being Element of K10(the carrier of A) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A9: not p = q ; :: thesis: ex b₁, b₂ being Element of K10(the carrier of A) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
( p = 0 & q = 0 ) by TARSKI:def 1;
hence ex b₁, b₂ being Element of K10(the carrier of A) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A9; :: thesis: verum