:: deftheorem defines Double ROBBINS1:def 17 :
for G being non empty ComplLLattStr
for x being Element of G holds Double x = x + x;