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