set sn = (RWNotIn-seq L) . n;
set FNI = n -thRWNotIn L;
A1: min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def 7;

now

assume n -thRWNotIn L = intloc 0 ; :: thesis: contradiction
then min ((RWNotIn-seq L) . n) = 0 by AMI_3:10;
hence contradiction by A1, Th18; :: thesis: verum

end;

hence not n -thRWNotIn L is read-only by SF_MASTR:def 5; :: thesis: verum