set sn = (RWNotIn-seq L) . n;
A1: min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def 7;
assume n -thRWNotIn L = intloc 0 ; :: according to SCMFSA_M:def 2 :: thesis: contradiction
then min ((RWNotIn-seq L) . n) = 0 by AMI_3:10;
hence contradiction by A1, Th22; :: thesis: verum