:: deftheorem defines Huntington ROBBINS1:def 12 :
for G being non empty join-commutative ComplLLattStr holds
( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y );