let L be finite Subset of FinSeq-Locations; :: thesis: not First*NotIn L in L
set FNI = First*NotIn L;
consider sn being non empty Subset of NAT such that
A1: First*NotIn L = fsloc (min sn) and
A2: sn = { k where k is Element of NAT : not fsloc k in L } by Def4;
min sn in sn by XXREAL_2:def 7;
then ex k being Element of NAT st
( k = min sn & not fsloc k in L ) by A2;
hence not First*NotIn L in L by A1; :: thesis: verum