JUMP (a >0_goto i1) = {i1} by Th51;
hence ( not JUMP (a >0_goto i1) is empty & JUMP (a >0_goto i1) is trivial ) ; :: thesis: verum