theorem Th4: :: LATTICE3:4

for X being set holds
( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )