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