let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: L is lower-bounded

ex c being Element of L st

for a being Element of L holds

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

ex c being Element of L st

for a being Element of L holds

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

proof

hence
L is lower-bounded
; :: thesis: verum
take
Bot' L
; :: thesis: for a being Element of L holds

( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )

let a be Element of L; :: thesis: ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )

thus ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) by Th5; :: thesis: verum

end;( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )

let a be Element of L; :: thesis: ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )

thus ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) by Th5; :: thesis: verum