let a be Data-Location ; :: thesis: for k being natural number holds JUMP (a >0_goto k) = {k}
let k be natural number ; :: thesis: JUMP (a >0_goto k) = {k}
set X = { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ;

now

let x be set ; :: thesis: ( ( x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ) )

A1: now

let Y be set ; :: thesis: ( Y in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } implies k in Y )
assume Y in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; :: thesis: k in Y
then consider il being Element of NAT such that
A2: Y = NIC ((a >0_goto k),il) ;
NIC ((a >0_goto k),il) = {k,(succ il)} by Th52;
hence k in Y by A2, TARSKI:def 2; :: thesis: verum

end;

hereby :: thesis: ( x in {k} implies x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } )

set il1 = 1;
set il2 = 2;
assume A3: x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; :: thesis: x in {k}
A4: NIC ((a >0_goto k),2) = {k,(succ 2)} by Th52;
NIC ((a >0_goto k),2) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ;
then x in NIC ((a >0_goto k),2) by A3, SETFAM_1:def 1;
then A5: ( x = k or x = succ 2 ) by A4, TARSKI:def 2;
A6: NIC ((a >0_goto k),1) = {k,(succ 1)} by Th52;
NIC ((a >0_goto k),1) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ;
then x in NIC ((a >0_goto k),1) by A3, SETFAM_1:def 1;
then ( x = k or x = succ 1 ) by A6, TARSKI:def 2;
hence x in {k} by A5, TARSKI:def 1; :: thesis: verum

end;

assume x in {k} ; :: thesis: x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum }
then A7: x = k by TARSKI:def 1;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
NIC ((a >0_goto k),k) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ;
hence x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } by A7, A1, SETFAM_1:def 1; :: thesis: verum

end;

hence JUMP (a >0_goto k) = {k} by TARSKI:1; :: thesis: verum