:: deftheorem defines AddTo SCMPDS_2:def 12 :
for a being Int_position
for k1, k2 being Integer holds AddTo (a,k1,k2) = [8,{},<*a,k1,k2*>];