let L be non empty Lattice-like Boolean LattStr ; :: thesis: L is upper-bounded'
ex c being Element of L st
for a being Element of L holds
( c "/\" a = a & a "/\" c = a )

proof

take c = Top L; :: thesis: for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
let a be Element of L; :: thesis: ( c "/\" a = a & a "/\" c = a )
a [= c by LATTICES:45;
hence ( c "/\" a = a & a "/\" c = a ) by LATTICES:21; :: thesis: verum

end;

hence L is upper-bounded' by Def1; :: thesis: verum