let X be set ; :: thesis: ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
A1: bool X = H₁( 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 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 ) by A1, XBOOLE_1:12; :: thesis: verum

end;

hence Top (BooleLatt X) = X by A2, A3, LATTICES:def 17; :: thesis: verum