:: deftheorem defines satisfying_MD_2 ROBBINS2:def 3 :
for L being non empty ComplLLattStr holds
( L is satisfying_MD_2 iff for x, y, z being Element of L holds (((x `) + y) `) + (z + y) = y + (z + x) );