:: deftheorem defines := SCMPDS_2:def 6 :
for a being Int_position
for k1 being Integer holds a := k1 = [2,{},<*a,k1*>];