( k2 = 5 or k2 <> 5 ) ;
hence JUMP (a,k1 <=0_goto k2) is empty by Lm11, Lm12; :: thesis: verum