let p be preProgram of SCM+FSA; :: thesis: not FirstNotUsed p in UsedIntLoc p
consider sil being finite Subset of Int-Locations such that
A1: sil = (UsedIntLoc p) \/ {(intloc 0)} and
A2: FirstNotUsed p = FirstNotIn sil by Def6;
not FirstNotUsed p in sil by A2, SCMFSA_M:14;
hence not FirstNotUsed p in UsedIntLoc p by A1, XBOOLE_0:def 3; :: thesis: verum