let i be Instruction of SCMPDS ; :: thesis: for l being Instruction-Location of SCMPDS st ( for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = Next (IC s) ) holds
NIC i,l = {(Next l)}
let l be Instruction-Location of SCMPDS ; :: thesis: ( ( for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = Next (IC s) ) implies NIC i,l = {(Next l)} )
assume A1: for s being State of SCMPDS st IC s = l & s . l = i holds
(Exec i,s) . (IC SCMPDS ) = Next (IC s) ; :: thesis: NIC i,l = {(Next l)}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Next l)} c= NIC i,l

let x be set ; :: thesis: ( x in NIC i,l implies x in {(Next l)} )
assume x in NIC i,l ; :: thesis: x in {(Next l)}
then consider s being State of SCMPDS such that
A2: ( x = IC (Following s) & IC s = l & s . l = i ) ;
x = (Exec (s . (IC s)),s) . (IC SCMPDS ) by A2, AMI_1:131
.= Next l by A1, A2 ;
hence x in {(Next l)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Next l)} or x in NIC i,l )
assume x in {(Next l)} ; :: thesis: x in NIC i,l
then A3: x = Next l by TARSKI:def 1;
consider t being State of SCMPDS ;
l in NAT by AMI_1:def 4;
then reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by AMI_1:def 11;
reconsider I = i as Element of ObjectKind l by AMI_1:def 14;
set u = t +* ((IC SCMPDS ),l --> il1,I);
A4: IC (t +* ((IC SCMPDS ),l --> il1,I)) = l by AMI_1:129;
A5: (t +* ((IC SCMPDS ),l --> il1,I)) . l = i by AMI_1:129;
IC (Following (t +* ((IC SCMPDS ),l --> il1,I))) = (Exec ((t +* ((IC SCMPDS ),l --> il1,I)) . (IC (t +* ((IC SCMPDS ),l --> il1,I)))),(t +* ((IC SCMPDS ),l --> il1,I))) . (IC SCMPDS ) by AMI_1:129
.= Next l by A1, A4, A5 ;
hence x in NIC i,l by A3, A4, A5; :: thesis: verum