theorem Th53: :: ROBBINS1:53

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