theorem :: SCMPDS_6:95

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;