theorem Th57: :: SF_MASTR:57

for p being preProgram of SCM+FSA holds not First*NotUsed p in UsedI*Loc p