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 )} & FirstNotUsed p = FirstNotIn sil ) by Def7;
not FirstNotUsed p in sil by A1, Th52;
hence not FirstNotUsed p in UsedIntLoc p by A1, XBOOLE_0:def 3; :: thesis: verum