let L be WA_Lattice; :: thesis: ( L is distributive' implies L is join-associative )
assume A0: L is distributive' ; :: thesis: L is join-associative
( L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative & L is satisfying_W3 & L is satisfying_W3' ) ;
then ( ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( 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 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 ) & ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) & ( for v0, v2, v1 being Element of L holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) ) by A0, ROBBINS3:def 3, LATTICES:def 9;
then for v0, v1, v2 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) by WALDistri;
hence L is join-associative by LATTICES:def 5; :: thesis: verum