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