for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0