{ k where k is Nat : k > 1 } is infinite by PRE_CIRC:23;
hence not JUMP (return a) is finite by Th17; :: thesis: verum