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