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