let X be set ; :: thesis: ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
A1: ( X in bool X & bool X = H₁( BooleLatt X) ) by Def1, ZFMISC_1:def 1;
then reconsider x = X as Element of (BooleLatt X) ;
A2: for y being Element of (BooleLatt X) holds
( x "\/" y = x & 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, LATTICES:def 17; :: thesis: verum