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