let X be set ; :: thesis: ( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} )
{} c= X ;
then reconsider x = {} as Element of (BooleLatt X) by Def1;
A1: for y being Element of (BooleLatt X) holds x "/\" y = x ;
A2: for y being Element of (BooleLatt X) holds y "/\" x = x ;
thus BooleLatt X is lower-bounded :: thesis: Bottom (BooleLatt X) = {}

proof

take x ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (BooleLatt X) holds
( x "/\" b₁ = x & b₁ "/\" x = x )
thus for b₁ being Element of the carrier of (BooleLatt X) holds
( x "/\" b₁ = x & b₁ "/\" x = x ) ; :: thesis: verum

end;

hence Bottom (BooleLatt X) = {} by A1, A2, LATTICES:def 16; :: thesis: verum