theorem :: SCMPDS_6:67

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