:: deftheorem defines dl. AMI_3:def 11 :
for k being Nat holds dl. k = [1,k];