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