let S be Hausdorff compact TopLattice; :: thesis: ( ( for x being Element of S holds x "/\" is continuous ) implies S is bounded )
assume A1: for x being Element of S holds x "/\" is continuous ; :: thesis: S is bounded
thus S is lower-bounded :: according to YELLOW_0:def 6 :: thesis: S is upper-bounded
proof
reconsider x = inf (S opp+id) as Element of S ;
take x ; :: according to YELLOW_0:def 4 :: thesis: x is_<=_than the carrier of S
A2: rng the mapping of (S opp+id) = rng (id S) by Def6
.= the carrier of S by RELAT_1:45 ;
then A3: x = "/\" ( the carrier of S,S) by YELLOW_2:def 6;
ex_inf_of S opp+id by A1, Th39;
then ex_inf_of the carrier of S,S by A2;
hence x is_<=_than the carrier of S by A3, YELLOW_0:31; :: thesis: verum
end;
reconsider x = sup (S +id) as Element of S ;
take x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of S is_<=_than x
A4: rng the mapping of (S +id) = rng (id S) by Def5
.= the carrier of S by RELAT_1:45 ;
then A5: x = "\/" ( the carrier of S,S) by YELLOW_2:def 5;
ex_sup_of S +id by A1, Th38;
then ex_sup_of the carrier of S,S by A4;
hence the carrier of S is_<=_than x by A5, YELLOW_0:30; :: thesis: verum