theorem :: SF_MASTR:48

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