let R be good Ring; :: thesis: for i1 being Element of NAT holds JUMP (goto i1,R) = {i1}
let i1 be Element of NAT ; :: thesis: JUMP (goto i1,R) = {i1}
set X = { (NIC (goto i1,R),il) where il is Element of NAT : verum } ;

now

let x be set ; :: thesis: ( ( x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum } ) )

hereby :: thesis: ( x in {i1} implies x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum } )

reconsider il1 = 1 as Element of NAT ;
A1: NIC (goto i1,R),il1 in { (NIC (goto i1,R),il) where il is Element of NAT : verum } ;
assume x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum } ; :: thesis: x in {i1}
then x in NIC (goto i1,R),il1 by A1, SETFAM_1:def 1;
hence x in {i1} by Th59; :: thesis: verum

end;

assume x in {i1} ; :: thesis: x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum }
then A2: x = i1 by TARSKI:def 1;

A3: now

let Y be set ; :: thesis: ( Y in { (NIC (goto i1,R),il) where il is Element of NAT : verum } implies i1 in Y )
assume Y in { (NIC (goto i1,R),il) where il is Element of NAT : verum } ; :: thesis: i1 in Y
then consider il being Element of NAT such that
A4: Y = NIC (goto i1,R),il ;
NIC (goto i1,R),il = {i1} by Th59;
hence i1 in Y by A4, TARSKI:def 1; :: thesis: verum

end;

NIC (goto i1,R),i1 in { (NIC (goto i1,R),il) where il is Element of NAT : verum } ;
hence x in meet { (NIC (goto i1,R),il) where il is Element of NAT : verum } by A2, A3, SETFAM_1:def 1; :: thesis: verum

end;

hence JUMP (goto i1,R) = {i1} by TARSKI:2; :: thesis: verum