consider sil being finite Subset of Int-Locations such that
A1: ( sil = (UsedIntLoc p) \/ {(intloc 0 )} & FirstNotUsed p = FirstNotIn sil ) by Def7;

now

assume FirstNotIn sil = intloc 0 ; :: thesis: contradiction
then not intloc 0 in sil by Th52;
hence contradiction by A1, SETWISEO:6; :: thesis: verum

end;

hence not FirstNotUsed p is read-only by A1, Def5; :: thesis: verum