reconsider C = bool {0 } as Subset-Family of {0 } ;
0 in {0 } by TARSKI:def 1;
then reconsider r = {[0 ,0 ]} as Relation of {0 } by RELSET_1:8;
{{} ,{0 }} = bool {0 } by ZFMISC_1:30;
then reconsider A = TopRelStr(# {0 },r,C #) as non empty trivial finite discrete reflexive TopRelStr by 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 A1: 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 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 A1, TARSKI:def 1; :: thesis: verum