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