:: deftheorem Def3 defines FirstNotIn SCMFSA_M:def 3 :
for L being finite Subset of Int-Locations
for b₂ being Int-Location holds
( b₂ = FirstNotIn L iff ex sn being non empty Subset of NAT st
( b₂ = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) );