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 )

ex c being Element of L st

for a being Element of L holds

( c "/\" a = a & a "/\" c = a )

proof

hence
L is upper-bounded'
; :: thesis: verum
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;( 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