theorem :: SCMFSA_M:16

for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L