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