let m, n be Nat; :: thesis: for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
let L be finite Subset of Int-Locations; :: thesis: ( FirstNotIn L = intloc m & not intloc n in L implies m <= n )
consider sn being non empty Subset of NAT such that
A1: ( FirstNotIn L = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) by Def3;
A2: n in NAT by ORDINAL1:def 12;
assume ( FirstNotIn L = intloc m & not intloc n in L ) ; :: thesis: m <= n
then ( m = min sn & n in sn ) by A1, AMI_3:10, A2;
hence m <= n by XXREAL_2:def 7; :: thesis: verum