let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' 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 Def5
.= ((x "\/" x) "/\" (x "\/" y)) "/\" (x "\/" z) by Def5
.= (x "/\" (x "\/" y)) "/\" (x "\/" z)
.= x "/\" (x "\/" z) by LATTICES:def 9
.= x by LATTICES:def 9 ;
hence ((x "/\" y) "/\" z) "\/" x = x ; :: thesis: verum