:: deftheorem Def4 defines First*NotIn SCMFSA_M:def 4 :
for L being finite Subset of FinSeq-Locations
for b₂ being FinSeq-Location holds
( b₂ = First*NotIn L iff ex sn being non empty Subset of NAT st
( b₂ = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) );