theorem Th49: :: ROBBINS1:49
for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0