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 )
A1: for k being Nat st S1[k] holds
k <= len W ;
assume that
A2: n is odd and
A3: n <= len W ; :: thesis: ex IT being odd Element of NAT st
( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT ) )

A4: ex k being Nat st S1[k] by A2, A3;
consider IT being Nat such that
A5: ( S1[IT] & ( for k being Nat st S1[k] holds
k <= IT ) ) from NAT_1:sch 6(A1, A4);
reconsider IT = IT as odd Element of NAT by ;
take IT = IT; :: thesis: ( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT ) )

thus ( IT <= len W & W . IT = W . n ) by A5; :: thesis: for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT

thus for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT by A5; :: 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