JUMP (goto (i1,R)) = {i1} by Th60;
hence JUMP (goto (i1,R)) is 1 -element ; :: thesis: verum