theorem Cluster1: :: LATQUASI:5

for L being non empty LattStr st 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 holds
L is distributive