let L be join-associative meet-absorbing Lattice; :: thesis: L is satisfying_W3'
for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1

proof

let v2, v1, v0 be Element of L; :: thesis: ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1
((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = (v0 "/\" v1) "\/" ((v2 "/\" v1) "\/" v1) by LATTICES:def 5
.= (v0 "/\" v1) "\/" v1 by LATTICES:def 8
.= v1 by LATTICES:def 8 ;
hence ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ; :: thesis: verum

end;

hence L is satisfying_W3' ; :: thesis: verum