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 )

proof

take c = Bot' L; :: thesis: for a being Element of L holds
( c "/\" a = c & a "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
thus ( c "/\" a = c & a "/\" c = c ) by Th6; :: thesis: verum

end;

hence L is lower-bounded by LATTICES:def 13; :: thesis: verum