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