consider s being State of S;
reconsider f = (IC S),l --> l,i as PartState of S by AMI_1:149;
IC (Following (ProgramPart (s +* f)),(s +* f)) in NIC i,l by Lm2;
hence not NIC i,l is empty ; :: thesis: verum