theorem Th50: :: SF_MASTR:50

for p being preProgram of SCM+FSA holds not FirstNotUsed p in UsedILoc p