for L being finite Subset of Int-Locations holds not FirstNotIn L in L by SCMFSA_M:14;