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