theorem :: SCMFSA_M:14

for L being finite Subset of Int-Locations holds not FirstNotIn L in L