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

proof

take c = Bottom 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 lower-bounded' ; :: thesis: verum