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