let L be non empty LattStr ; ( L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-distributive implies L is distributive )
assume that
A1:
L is meet-commutative
and
A2:
L is satisfying_QLT1
and
A3:
L is join-idempotent
and
A4:
L is join-associative
and
A5:
L is join-commutative
and
A6:
L is satisfying_QLT2
and
A7:
L is QLT-distributive
; L is distributive
S:
for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0
by LATTICES:def 6, A1;
S2:
for v0 being Element of L holds v0 "\/" v0 = v0
by A3, ROBBINS1:def 7;
S3:
for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2)
by A4, LATTICES:def 5;
S4:
for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0
by A5, LATTICES:def 4;
let v1, v2, v3 be Element of L; LATTICES:def 11 v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3)
thus
v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3)
by Lemma1, S, A2, A6, S2, S3, S4, A7; verum