:: deftheorem defines -thRWNotIn SCMFSA_M:def 6 :
for n being Element of NAT
for L being finite Subset of Int-Locations holds n -thRWNotIn L = intloc (min ((RWNotIn-seq L) . n));