let p be preProgram of SCM+FSA ; :: thesis: not First*NotUsed p in UsedInt*Loc p
consider sil being finite Subset of FinSeq-Locations such that
A1: ( sil = UsedInt*Loc p & First*NotUsed p = First*NotIn sil ) by Def9;
thus not First*NotUsed p in UsedInt*Loc p by A1, Th59; :: thesis: verum