let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; :: thesis: for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x
let x, y, z be Element of L; :: thesis: ((x "\/" y) "\/" z) "/\" x = x
((x "\/" y) "\/" z) "/\" x = (x "/\" (x "\/" y)) "\/" (x "/\" z) by LATTICES:def 11
.= ((x "/\" x) "\/" (x "/\" y)) "\/" (x "/\" z) by LATTICES:def 11
.= (x "\/" (x "/\" y)) "\/" (x "/\" z)
.= x "\/" (x "/\" z) by LATTICES:def 8
.= x by LATTICES:def 8 ;
hence ((x "\/" y) "\/" z) "/\" x = x ; :: thesis: verum