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 ;
S2: for v0 being Element of L holds v0 "\/" v0 = v0 by ;
S3: for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) by ;
S4: for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 by ;
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