theorem :: ROBBINS1:39

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