theorem Th17: :: SCMPDS_9:17

for a being Int_position holds JUMP (return a) = { k where k is Nat : k > 1 }