:: deftheorem defines AddTo SCMRING2:def 4 :
for R being Ring
for a, b being Data-Location of R holds AddTo (a,b) = [2,{},<*a,b*>];