let k be Integer; :: thesis: JUMP (goto k) = {}
set i = goto k;
set X = { (NIC ((goto k),l)) where l is Element of NAT : verum } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= JUMP (goto k)

set l2 = 1;
set l1 = 0 ;
let x be set ; :: thesis: ( x in JUMP (goto k) implies b₁ in {} )
assume A1: x in JUMP (goto k) ; :: thesis: b₁ in {}
NIC ((goto k),1) in { (NIC ((goto k),l)) where l is Element of NAT : verum } ;
then x in NIC ((goto k),1) by A1, SETFAM_1:def 1;
then consider s2 being Element of product the Object-Kind of SCMPDS such that
A2: x = IC (Exec ((goto k),s2)) and
A3: IC s2 = 1 ;
consider m2 being Element of NAT such that
A4: m2 = IC s2 and
A5: ICplusConst (s2,k) = abs (m2 + k) by SCMPDS_2:def 18;
NIC ((goto k),0) in { (NIC ((goto k),l)) where l is Element of NAT : verum } ;
then x in NIC ((goto k),0) by A1, SETFAM_1:def 1;
then consider s1 being Element of product the Object-Kind of SCMPDS such that
A6: x = IC (Exec ((goto k),s1)) and
A7: IC s1 = 0 ;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,k) = abs (m1 + k) by SCMPDS_2:def 18;
A10: x = abs (m1 + k) by A6, A9, SCMPDS_2:54;

per cases ( 0 + k = 1 + k or k = - (1 + k) ) by A7, A8, A10, A3, A4, A2, A5, ABSVALUE:28, SCMPDS_2:54;

suppose 0 + k = 1 + k ; :: thesis: b₁ in {}

hence x in {} ; :: thesis: verum

end;

suppose k = - (1 + k) ; :: thesis: b₁ in {}

then - (- (1 / 2)) is integer ;
hence x in {} by NAT_D:33; :: thesis: verum

end;

end;

end;

thus {} c= JUMP (goto k) by XBOOLE_1:2; :: thesis: verum