theorem :: SCMPDS_6:56

for a being Int_position
for k1 being Integer
for I being Program of holds
( 0 in dom (if<>0 (a,k1,I)) & 1 in dom (if<>0 (a,k1,I)) ) by Lm9;