:: deftheorem defines saveIC SCMPDS_2:def 7 :
for a being Int_position
for k1 being Integer holds saveIC (a,k1) = [3,{},<*a,k1*>];