let L be finite Subset of Int-Locations; :: thesis: for n being Nat holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
let n be Nat; :: thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
set RL = RWNotIn-seq L;
set sn = (RWNotIn-seq L) . n;
set sn1 = (RWNotIn-seq L) . (n + 1);
assume A1: min ((RWNotIn-seq L) . n) >= min ((RWNotIn-seq L) . (n + 1)) ; :: thesis: contradiction
A2: (RWNotIn-seq L) . (n + 1) = ((RWNotIn-seq L) . n) \ {(min ((RWNotIn-seq L) . n))} by Def5;
then min ((RWNotIn-seq L) . n) <= min ((RWNotIn-seq L) . (n + 1)) by XBOOLE_1:36, XXREAL_2:60;
then min ((RWNotIn-seq L) . n) = min ((RWNotIn-seq L) . (n + 1)) by A1, XXREAL_0:1;
then A3: min ((RWNotIn-seq L) . (n + 1)) in {(min ((RWNotIn-seq L) . n))} by TARSKI:def 1;
min ((RWNotIn-seq L) . (n + 1)) in (RWNotIn-seq L) . (n + 1) by XXREAL_2:def 7;
hence contradiction by A2, A3, XBOOLE_0:def 5; :: thesis: verum