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