theorem :: SF_MASTR:55

for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L by SCMFSA_M:16;