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 b1 being Element of the carrier of (BooleLatt X) holds
( x "/\" b1 = x & b1 "/\" x = x )
thus for b1 being Element of the carrier of (BooleLatt X) holds
( x "/\" b1 = x & b1 "/\" x = x ) ; :: thesis: verum
end;
hence Bottom (BooleLatt X) = {} by A1, A2, LATTICES:def 16; :: thesis: verum