theorem :: SCMFSA_M:17

for m, n being Nat
for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n