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

now

let x be set ; :: thesis: ( ( x in meet { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : 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+FSA : verum } ) )

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

assume A1: x in meet { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : verum } ; :: thesis: x in {i1}
set il1 = insloc 1;
set il2 = insloc 2;
( NIC (a =0_goto i1),(insloc 1) in { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : verum } & NIC (a =0_goto i1),(insloc 2) in { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : verum } ) ;
then A2: ( x in NIC (a =0_goto i1),(insloc 1) & x in NIC (a =0_goto i1),(insloc 2) ) by A1, SETFAM_1:def 1;
( NIC (a =0_goto i1),(insloc 1) = {i1,(Next (insloc 1))} & NIC (a =0_goto i1),(insloc 2) = {i1,(Next (insloc 2))} ) by Th76;
then ( ( x = i1 or x = Next (insloc 1) ) & ( x = i1 or x = Next (insloc 2) ) ) by A2, TARSKI:def 2;
hence x in {i1} by 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+FSA : verum }
then A3: x = i1 by TARSKI:def 1;
A4: NIC (a =0_goto i1),i1 in { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : verum } ;

now

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

end;

hence x in meet { (NIC (a =0_goto i1),il) where il is Instruction-Location of SCM+FSA : verum } by A3, A4, SETFAM_1:def 1; :: thesis: verum

end;

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