:: deftheorem DefD defines Distributive LATTAD_1:def 1 :
for L being non empty LattStr holds
( L is Distributive iff for x, y, z being Element of L holds (x "\/" y) "/\" z = (x "/\" z) "\/" (y "/\" z) );