for L being finite Subset of Int-Locations
for n, m being Element of NAT st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)