let L be non empty LattStr ; :: thesis: ( L is meet-commutative & L is join-idempotent & L is join-commutative & L is satisfying_W3' implies L is meet-Absorbing )
assume ( L is meet-commutative & L is join-idempotent & L is join-commutative & L is satisfying_W3' ) ; :: thesis: L is meet-Absorbing
then ( ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) ) by LATTICES:def 4, LATTICES:def 6;
then for v1, v2 being Element of L holds v1 "\/" (v1 "/\" v2) = v1 by Lemma4;
hence L is meet-Absorbing by ROBBINS3:def 3; :: thesis: verum