let X be set ; :: thesis: ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
A1: bool X = H1( BooleLatt X) by Def1;
then reconsider x = X as Element of (BooleLatt X) by ZFMISC_1:def 1;
A2: for y being Element of (BooleLatt X) holds x "\/" y = x by A1, XBOOLE_1:12;
A3: for y being Element of (BooleLatt X) holds y "\/" x = x by A1, XBOOLE_1:12;
thus BooleLatt X is upper-bounded :: thesis: Top (BooleLatt X) = X
proof
take x ; :: according to LATTICES:def 14 :: 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 ) by A1, XBOOLE_1:12; :: thesis: verum
end;
hence Top (BooleLatt X) = X by A2, A3, LATTICES:def 17; :: thesis: verum