consider sil being finite Subset of Int-Locations such that
A1: sil = (UsedIntLoc p) \/ {(intloc 0 )} and
A2: 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 A2, Def5; :: thesis: verum