let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; :: thesis: for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q
let p, q, r be Element of L; :: thesis: ( p [= q implies r "\/" p [= r "\/" q )
assume A1: p "\/" q = q ; :: according to LATTICES:def 3 :: thesis: r "\/" p [= r "\/" q
thus (r "\/" p) "\/" (r "\/" q) = (r "\/" (r "\/" p)) "\/" q by LATTICES:def 5
.= ((r "\/" r) "\/" p) "\/" q by LATTICES:def 5
.= (r "\/" p) "\/" q
.= r "\/" q by A1, LATTICES:def 5 ; :: according to LATTICES:def 3 :: thesis: verum