:: deftheorem defines Double MIDSP_2:def 1 :
for G being non empty addLoopStr
for x being Element of G holds Double x = x + x;