for n being Nat
for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )