:: deftheorem Def6 defines Huntington ROBBINS1:def 6 :
for L being non empty ComplLLattStr holds
( L is Huntington iff for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x );