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 )
thus ( c "/\" a = a & a "/\" c = a ) ; :: thesis: verum

end;

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