:: deftheorem Def11 defines distributive LATTICES:def 11 :
for IT being non empty LattStr holds
( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) );