let p be preProgram of SCM+FSA; :: thesis: not FirstNotUsed p in UsedILoc p

consider sil being finite Subset of Int-Locations such that

A1: sil = (UsedILoc p) \/ {(intloc 0)} and

A2: FirstNotUsed p = FirstNotIn sil by Def7;

not FirstNotUsed p in sil by A2, SCMFSA_M:14;

hence not FirstNotUsed p in UsedILoc p by A1, XBOOLE_0:def 3; :: thesis: verum

consider sil being finite Subset of Int-Locations such that

A1: sil = (UsedILoc p) \/ {(intloc 0)} and

A2: FirstNotUsed p = FirstNotIn sil by Def7;

not FirstNotUsed p in sil by A2, SCMFSA_M:14;

hence not FirstNotUsed p in UsedILoc p by A1, XBOOLE_0:def 3; :: thesis: verum