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