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:3;
{{},{0}} = bool {0} by ZFMISC_1:24;
then reconsider A = TopRelStr(# {0},r,C #) as finite 1 -element discrete reflexive TopRelStr by Lm4;
reconsider A = A as TopLattice ;
take A ; :: thesis: ( A is strict & A is discrete & A is finite & A is compact & A is Hausdorff & A is 1 -element )
thus ( A is strict & A is discrete & A is finite ) ; :: thesis: ( A is compact & A is Hausdorff & A is 1 -element )
thus A is compact ; :: thesis: ( A is Hausdorff & A is 1 -element )
thus A is Hausdorff :: thesis: A is 1 -element

proof

let p, q be Point of A; :: according to PRE_TOPC:def 10 :: 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

end;

thus A is 1 -element ; :: thesis: verum