theorem :: SCMFSA_M:15

for m, n being Nat
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n