let k be Nat; :: thesis: JUMP (SCM-goto k) = {k}
set X = { (NIC ((SCM-goto k),il)) where il is Nat : verum } ;

now :: thesis: for x being object holds
( ( x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } ) )

let x be object ; :: thesis: ( ( x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } ) )

hereby :: thesis: ( x in {k} implies x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } )

set il1 = 1;
A1: NIC ((SCM-goto k),1) in { (NIC ((SCM-goto k),il)) where il is Nat : verum } ;
assume x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } ; :: thesis: x in {k}
then x in NIC ((SCM-goto k),1) by A1, SETFAM_1:def 1;
hence x in {k} by Th15; :: thesis: verum

end;

assume x in {k} ; :: thesis: x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum }
then A2: x = k by TARSKI:def 1;

A3: now :: thesis: for Y being set st Y in { (NIC ((SCM-goto k),il)) where il is Nat : verum } holds
k in Y

let Y be set ; :: thesis: ( Y in { (NIC ((SCM-goto k),il)) where il is Nat : verum } implies k in Y )
assume Y in { (NIC ((SCM-goto k),il)) where il is Nat : verum } ; :: thesis: k in Y
then consider il being Nat such that
A4: Y = NIC ((SCM-goto k),il) ;
NIC ((SCM-goto k),il) = {k} by Th15;
hence k in Y by A4, TARSKI:def 1; :: thesis: verum

end;

reconsider k = k as Element of NAT by ORDINAL1:def 12;
NIC ((SCM-goto k),k) in { (NIC ((SCM-goto k),il)) where il is Nat : verum } ;
hence x in meet { (NIC ((SCM-goto k),il)) where il is Nat : verum } by A2, A3, SETFAM_1:def 1; :: thesis: verum

end;

hence JUMP (SCM-goto k) = {k} by TARSKI:2; :: thesis: verum