:: deftheorem defines := SCMRING2:def 3 :
for R being Ring
for a, b being Data-Location of R holds a := b = [1,{},<*a,b*>];