let L be non empty LattStr ; :: thesis: ( 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 ; :: thesis: 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; :: according to LATTICES:def 11 :: thesis: v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3)

thus v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3) by Lemma1, S, A2, A6, S2, S3, S4, A7; :: thesis: verum

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 ; :: thesis: 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; :: according to LATTICES:def 11 :: thesis: v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3)

thus v1 "/\" (v2 "\/" v3) = (v1 "/\" v2) "\/" (v1 "/\" v3) by Lemma1, S, A2, A6, S2, S3, S4, A7; :: thesis: verum