let m, n be Nat; :: thesis: for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
let L be finite Subset of FinSeq-Locations; :: thesis: ( First*NotIn L = fsloc m & not fsloc n in L implies m <= n )
assume that
A1: First*NotIn L = fsloc m and
A2: not fsloc n in L ; :: thesis: m <= n
consider sn being non empty Subset of NAT such that
A3: First*NotIn L = fsloc (min sn) and
A4: sn = { k where k is Element of NAT : not fsloc k in L } by Def4;
n in NAT by ORDINAL1:def 12;
then n in sn by A2, A4;
hence m <= n by A1, A3, XXREAL_2:def 7; :: thesis: verum