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