set s = the State of S;
reconsider f = ((IC ),l) --> (l,i) as PartState of S by COMPOS_1:37;
IC (Following ((ProgramPart ( the State of S +* f)),( the State of S +* f))) in NIC (i,l) by Lm1;
hence not NIC (i,l) is empty ; :: thesis: verum