theorem :: SF_MASTR:56

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