theorem :: SCMPDS_6:65

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