JUMP (a >0_goto i1) = {i1} by Th38;
hence JUMP (a >0_goto i1) is 1 -element ; :: thesis: verum