defpred S₁[ 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 b₁ being odd Element of NAT st b₁ = len W )

A1: for k being Nat st S₁[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 S₁[k] by A2, A3;
consider IT being Nat such that
A5: ( S₁[IT] & ( for k being Nat st S₁[k] holds
k <= IT ) ) from NAT_1:sch 6(A1, A4);
reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 12;
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 b₁ being odd Element of NAT st b₁ = len W ) ; :: thesis: verum