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