defpred S1[ Nat] means ( $1 is odd & $1 <= len W & W . $1 = W . n );
hereby :: thesis: ( ( not n is odd or not n <= len W ) implies ex b1 being odd Element of NAT st b1 = len W )
assume that
A1: n is odd and
A2: n <= len W ; :: thesis: ex IT being odd Element of NAT st
( IT <= len W & W . IT = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
IT <= k ) )
A3: ex n being Nat st S1[n] by A1, A2;
consider IT being Nat such that
A4: ( S1[IT] & ( for k being Nat st S1[k] holds
IT <= k ) ) from NAT_1:sch 5(A3);
reconsider IT = IT as odd Element of NAT by A4, ORDINAL1:def 12;
take IT = IT; :: thesis: ( IT <= len W & W . IT = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
IT <= k ) )
thus ( IT <= len W & W . IT = W . n ) by A4; :: thesis: for k being odd Nat st k <= len W & W . k = W . n holds
IT <= k
let k be odd Nat; :: thesis: ( k <= len W & W . k = W . n implies IT <= k )
thus ( k <= len W & W . k = W . n implies IT <= k ) by A4; :: thesis: verum
end;
thus ( ( not n is odd or not n <= len W ) implies ex b1 being odd Element of NAT st b1 = len W ) ; :: thesis: verum