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