let p be preProgram of ; :: thesis: not First*NotUsed p in UsedInt*Loc p
ex sil being finite Subset of 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