for L being finite Subset of Int-Locations
for n, m being Element of NAT st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L