theorem Cluster2: :: LATQUASI:7

for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is join-idempotent & L is join-associative & L is satisfying_QLT2 & L is distributive holds
L is distributive'