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 :: thesis: for n being Element of NAT
for n being Nat holds S₁[n]

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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: ( 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 A3: n <= m by NAT_1:13;

per cases ( n = m or n < m ) by A3, 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 Th23; :: 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 A2, Th23, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A4: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1); :: thesis: verum

end;

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