let L be non empty LattStr ; :: thesis: ( L is meet-commutative & L is meet-idempotent & L is join-commutative & L is satisfying_W3 implies L is join-absorbing )
assume ( L is meet-commutative & L is meet-idempotent & L is join-commutative & L is satisfying_W3 ) ; :: thesis: L is join-absorbing
then Z1: ( ( 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;
for v1, v2 being Element of L holds v1 "/\" (v1 "\/" v2) = v1

proof

let v1, v2 be Element of L; :: thesis: v1 "/\" (v1 "\/" v2) = v1
((v2 "\/" v1) "/\" (v2 "\/" v1)) "/\" v1 = v1 by Z1;
then z2: ((v1 "\/" v2) "/\" (v2 "\/" v1)) "/\" v1 = v1 by Z1;
v1 "/\" (v1 "\/" v2) = (v1 "\/" v2) "/\" v1 by Z1
.= ((v1 "\/" v2) "/\" (v1 "\/" v2)) "/\" v1 by Z1
.= v1 by z2, Z1 ;
hence v1 "/\" (v1 "\/" v2) = v1 ; :: thesis: verum

end;

hence L is join-absorbing by LATTICES:def 9; :: thesis: verum