for L being finite Subset of Int-Locations
for n being Nat holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))