let n be Element of NAT ; :: thesis: for L being finite Subset of Int-Locations holds not n -thRWNotIn L in L
let L be finite Subset of Int-Locations; :: 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 Th18; :: thesis: verum