thus
( L is modular implies for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
by ClusterA; :: thesis: ( ( for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) ) implies L is modular )

SS: ( L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies L is modular ) by ClusterB;

assume for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) ; :: thesis: L is modular

hence L is modular by SS; :: thesis: verum

SS: ( L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) implies L is modular ) by ClusterB;

assume for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) ; :: thesis: L is modular

hence L is modular by SS; :: thesis: verum