:: deftheorem defines \beta ROBBINS1:def 22 :
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \beta x = ((- ((x _1) + (x _3))) + x) + (- (x _3));