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 (Following (ProgramPart s2),s2) and
A3: IC s2 = 1 and
A4: (ProgramPart s2) /. 1 = goto k ;
consider m2 being Element of NAT such that
A5: m2 = IC s2 and
A6: ICplusConst s2,k = abs (m2 + k) by SCMPDS_2:def 20;
A7: x = (Following (ProgramPart s2),s2) . (IC SCMPDS ) by A2, AMI_1:def 15
.= (Exec (CurInstr (ProgramPart s2),s2),s2) . (IC SCMPDS ) by AMI_1:def 18
.= (Exec (goto k),s2) . (IC SCMPDS ) by A3, A4, AMI_1:def 16
.= abs (m2 + k) by A6, SCMPDS_2:66 ;
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
A8: x = IC (Following (ProgramPart s1),s1) and
A9: IC s1 = 0 and
A10: (ProgramPart s1) /. 0 = goto k ;
consider m1 being Element of NAT such that
A11: m1 = IC s1 and
A12: ICplusConst s1,k = abs (m1 + k) by SCMPDS_2:def 20;
A13: x = (Following (ProgramPart s1),s1) . (IC SCMPDS ) by A8, AMI_1:def 15
.= (Exec (CurInstr (ProgramPart s1),s1),s1) . (IC SCMPDS ) by AMI_1:def 18
.= (Exec (goto k),s1) . (IC SCMPDS ) by A9, A10, AMI_1:def 16
.= abs (m1 + k) by A12, SCMPDS_2:66 ;

per cases ( 0 + k = 1 + k or k = - (1 + k) ) by A9, A11, A13, A3, A5, A7, ABSVALUE:45;

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