theorem :: SCMPDS_6:107

for a being Int_position
for k1 being Integer
for I being Program of holds (if<0 (a,k1,I)) . 0 = (a,k1) >=0_goto ((card I) + 1) by Th2;