let L be finite Subset of Int-Locations ; :: thesis: for n, m being Element of NAT st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)
let n, m be Element of NAT ; :: thesis: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) )
set RL = RWNotIn-seq L;

now

let n be Element of NAT ; :: thesis: for n being Element of NAT holds S₁[n]
defpred S₁[ Element of NAT ] means ( n < $1 implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . $1) );
A1: S₁[ 0 ] by NAT_1:2;
A2: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; :: thesis: S₁[m + 1]
assume n < m + 1 ; :: thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
then A4: n <= m by NAT_1:13;

per cases ( n = m or n < m ) by A4, XXREAL_0:1;

suppose n = m ; :: thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))

hence min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by Th19; :: thesis: verum

end;

suppose n < m ; :: thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))

hence min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by A3, Th19, XXREAL_0:2; :: thesis: verum

end;

end;

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2); :: thesis: verum

end;

hence ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; :: thesis: verum