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