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

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