let L be finite Subset of Int-Locations ; :: thesis: for n being Element of NAT holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
let n be Element of 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);
A1: (RWNotIn-seq L) . (n + 1) = ((RWNotIn-seq L) . n) \ {(min ((RWNotIn-seq L) . n))} by Def2;
A2: ( min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n & min ((RWNotIn-seq L) . (n + 1)) in (RWNotIn-seq L) . (n + 1) ) by XXREAL_2:def 7;
A3: min ((RWNotIn-seq L) . n) <= min ((RWNotIn-seq L) . (n + 1)) by A1, XBOOLE_1:36, XXREAL_2:60;
assume min ((RWNotIn-seq L) . n) >= min ((RWNotIn-seq L) . (n + 1)) ; :: thesis: contradiction
then min ((RWNotIn-seq L) . n) = min ((RWNotIn-seq L) . (n + 1)) by A3, XXREAL_0:1;
then min ((RWNotIn-seq L) . (n + 1)) in {(min ((RWNotIn-seq L) . n))} by TARSKI:def 1;
hence contradiction by A1, A2, XBOOLE_0:def 5; :: thesis: verum