theorem :: SCMPDS_2:18

for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) >=0_goto k2) = 6 ;