theorem :: SF_MASTR:49

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 by SCMFSA_M:15;