let p be preProgram of SCM+FSA; :: thesis: not First*NotUsed p in UsedInt*Loc p
ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p & First*NotUsed p = First*NotIn sil ) by Def9;
hence not First*NotUsed p in UsedInt*Loc p by Th59; :: thesis: verum