consider sil being finite Subset of Int-Locations such that

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

A2: FirstNotUsed p = FirstNotIn sil by Def7;

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

A2: FirstNotUsed p = FirstNotIn sil by Def7;

now :: thesis: not FirstNotIn sil = intloc 0

hence
not FirstNotUsed p is read-only
by A2, SCMFSA_M:def 2; :: thesis: verumassume
FirstNotIn sil = intloc 0
; :: thesis: contradiction

then not intloc 0 in sil by SCMFSA_M:14;

hence contradiction by A1, ZFMISC_1:136; :: thesis: verum

end;then not intloc 0 in sil by SCMFSA_M:14;

hence contradiction by A1, ZFMISC_1:136; :: thesis: verum