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 )
c [= a by LATTICES:16;
hence ( c "\/" a = a & a "\/" c = a ) by LATTICES:def 3; :: thesis: verum

end;

hence L is lower-bounded' by Def3; :: thesis: verum