let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for il being Instruction-Location of S
for i being Instruction of S st i is halting holds
NIC i,il = {il}
let IL be non empty set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for il being Instruction-Location of S
for i being Instruction of S st i is halting holds
NIC i,il = {il}
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for il being Instruction-Location of S
for i being Instruction of S st i is halting holds
NIC i,il = {il}
let il be Instruction-Location of S; :: thesis: for i being Instruction of S st i is halting holds
NIC i,il = {il}
let i be Instruction of S; :: thesis: ( i is halting implies NIC i,il = {il} )
assume A1: for s being State of S holds Exec i,s = s ; :: according to AMI_1:def 8 :: thesis: NIC i,il = {il}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {il} c= NIC i,il

let n be set ; :: thesis: ( n in NIC i,il implies n in {il} )
assume n in NIC i,il ; :: thesis: n in {il}
then consider s being State of S such that
A2: ( n = IC (Following s) & IC s = il & s . il = i ) ;
n = il by A1, A2;
hence n in {il} by TARSKI:def 1; :: thesis: verum

end;

let n be set ; :: according to TARSKI:def 3 :: thesis: ( not n in {il} or n in NIC i,il )
assume A3: n in {il} ; :: thesis: n in NIC i,il
A4: il in IL by AMI_1:def 4;
consider s being State of S;
( ObjectKind (IC S) = IL & ObjectKind il = the Instructions of S ) by AMI_1:def 11, AMI_1:def 14;
then reconsider f = (IC S),il --> il,i as FinPartState of S by A4, AMI_1:58;
set a = s +* f;
A5: dom f = {(IC S),il} by FUNCT_4:65;
then A6: IC S in dom f by TARSKI:def 2;
A7: il in dom f by A5, TARSKI:def 2;
A9: (s +* f) . (IC S) = f . (IC S) by A6, FUNCT_4:14
.= il by AMI_1:48, FUNCT_4:66 ;
then (s +* f) . (IC (s +* f)) = f . il by A7, FUNCT_4:14
.= i by FUNCT_4:66 ;
then IC (Following (s +* f)) = (s +* f) . (IC S) by A1
.= n by A3, A9, TARSKI:def 1 ;
hence n in NIC i,il by Lm2; :: thesis: verum