JUMP (goto (i1,R)) = {i1} by Th60;
hence ( not JUMP (goto (i1,R)) is empty & JUMP (goto (i1,R)) is trivial ) ; :: thesis: verum