let a be Data-Location ; :: thesis: for i1 being Instruction-Location of SCM holds JUMP (a >0_goto i1) = {i1}
let i1 be Instruction-Location of SCM ; :: thesis: JUMP (a >0_goto i1) = {i1}
set X = { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ;

now

let x be set ; :: thesis: ( ( x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ) )

A1: now

let Y be set ; :: thesis: ( Y in { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } implies i1 in Y )
assume Y in { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ; :: thesis: i1 in Y
then consider il being Instruction-Location of SCM such that
A2: Y = NIC (a >0_goto i1),il ;
NIC (a >0_goto i1),il = {i1,(Next )} by Th50;
hence i1 in Y by A2, TARSKI:def 2; :: thesis: verum

end;

hereby :: thesis: ( x in {i1} implies x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } )

set il1 = il. 1;
set il2 = il. 2;
assume A3: x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ; :: thesis: x in {i1}
A4: NIC (a >0_goto i1),(il. 2) = {i1,(Next )} by Th50;
NIC (a >0_goto i1),(il. 2) in { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ;
then x in NIC (a >0_goto i1),(il. 2) by A3, SETFAM_1:def 1;
then A5: ( x = i1 or x = Next ) by A4, TARSKI:def 2;
A6: NIC (a >0_goto i1),(il. 1) = {i1,(Next )} by Th50;
NIC (a >0_goto i1),(il. 1) in { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ;
then x in NIC (a >0_goto i1),(il. 1) by A3, SETFAM_1:def 1;
then ( x = i1 or x = Next ) by A6, TARSKI:def 2;
hence x in {i1} by A5, TARSKI:def 1; :: thesis: verum

end;

assume x in {i1} ; :: thesis: x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum }
then A7: x = i1 by TARSKI:def 1;
NIC (a >0_goto i1),i1 in { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } ;
hence x in meet { (NIC (a >0_goto i1),il) where il is Instruction-Location of SCM : verum } by A7, A1, SETFAM_1:def 1; :: thesis: verum

end;

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