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 7
.= (v0 "\/" v1) "/\" v1 by LATTICES:def 9
.= v1 by LATTICES:def 9 ;
hence ((v0 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 ; :: thesis: verum

end;

hence L is satisfying_W3 by LATWAL_1:def 1; :: thesis: verum