not { k where k is Element of NAT : k > 1 } is finite by PRE_CIRC:23;
hence not JUMP (return a) is finite by Th23; :: thesis: verum