let L be finite Subset of Int-Locations; :: thesis: for n, m being Element of NAT st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
let n, m be Element of NAT ; :: thesis: ( n <> m implies n -thRWNotIn L <> m -thRWNotIn L )
assume n <> m ; :: thesis: n -thRWNotIn L <> m -thRWNotIn L
then ( n < m or m < n ) by XXREAL_0:1;
then A1: min ((RWNotIn-seq L) . n) <> min ((RWNotIn-seq L) . m) by Th24;
assume n -thRWNotIn L = m -thRWNotIn L ; :: thesis: contradiction
hence contradiction by A1, AMI_3:10; :: thesis: verum