reconsider p = 0 , q = 1 as Element of NAT ;
let i be Instruction of ; :: thesis: ( ( for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ) implies JUMP i is empty )
assume A1: for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ; :: thesis: JUMP i is empty
set X = { (NIC i,f) where f is Instruction-Location of SCM+FSA : verum } ;
reconsider p = p, q = q as Instruction-Location of SCM+FSA by AMI_1:def 4;
assume not JUMP i is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in meet { (NIC i,f) where f is Instruction-Location of SCM+FSA : verum } by XBOOLE_0:def 1;
NIC i,p = {(Next p)} by A1;
then {(Next p)} in { (NIC i,f) where f is Instruction-Location of SCM+FSA : verum } ;
then x in {(Next p)} by A2, SETFAM_1:def 1;
then A3: x = Next p by TARSKI:def 1;
NIC i,q = {(Next q)} by A1;
then {(Next q)} in { (NIC i,f) where f is Instruction-Location of SCM+FSA : verum } ;
then x in {(Next q)} by A2, SETFAM_1:def 1;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum