let n be Nat; :: thesis: for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
let L be finite Subset of Int-Locations; :: thesis: ( not 0 in (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
set RL = RWNotIn-seq L;
defpred S₁[ Nat] means ( not 0 in (RWNotIn-seq L) . $1 & ( for m being Nat st m in (RWNotIn-seq L) . $1 holds
not intloc m in L ) );
A1: S₁[ 0 ]

proof

A2: (RWNotIn-seq L) . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } by Def5;

hereby :: thesis: for m being Nat st m in (RWNotIn-seq L) . 0 holds
not intloc m in L

assume 0 in (RWNotIn-seq L) . 0 ; :: thesis: contradiction
then ex k being Element of NAT st
( k = 0 & not intloc k in L & k <> 0 ) by A2;
hence contradiction ; :: thesis: verum

end;

let m be Nat; :: thesis: ( m in (RWNotIn-seq L) . 0 implies not intloc m in L )
assume m in (RWNotIn-seq L) . 0 ; :: thesis: not intloc m in L
then ex k being Element of NAT st
( k = m & not intloc k in L & k <> 0 ) by A2;
hence not intloc m in L ; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A4: not 0 in (RWNotIn-seq L) . n and
A5: for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ; :: thesis: S₁[n + 1]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider sn = (RWNotIn-seq L) . nn as non empty Subset of NAT ;
A6: (RWNotIn-seq L) . (n + 1) = sn \ {(min sn)} by Def5;
hence not 0 in (RWNotIn-seq L) . (n + 1) by A4, XBOOLE_0:def 5; :: thesis: for m being Nat st m in (RWNotIn-seq L) . (n + 1) holds
not intloc m in L
let m be Nat; :: thesis: ( m in (RWNotIn-seq L) . (n + 1) implies not intloc m in L )
assume m in (RWNotIn-seq L) . (n + 1) ; :: thesis: not intloc m in L
then m in (RWNotIn-seq L) . n by A6, XBOOLE_0:def 5;
hence not intloc m in L by A5; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence ( not 0 in (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ) ) ; :: thesis: verum