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 b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1: not p = q ; :: thesis: ex b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
p = 0 by TARSKI:def 1;
hence ex b1, b2 being Element of K10( the carrier of A) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A1, TARSKI:def 1; :: thesis: verum
end;
thus A is 1 -element ; :: thesis: verum