let L be finite Subset of Int-Locations; :: thesis: for n being Element of NAT holds not n -thRWNotIn L in L
let n be Element of NAT ; :: thesis: not n -thRWNotIn L in L
set FNI = n -thRWNotIn L;
set sn = (RWNotIn-seq L) . n;
min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def 7;
hence not n -thRWNotIn L in L by Th22; :: thesis: verum