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