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

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