defpred S₁[ Nat] means ( not $1 is even & $1 <= len W & W . $1 = W . n );

hereby :: thesis: ( ( n is even or not n <= len W ) implies ex b₁ being odd Element of NAT st b₁ = len W )

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

end;

thus ( ( n is even or not n <= len W ) implies ex b₁ being odd Element of NAT st b₁ = len W ) ; :: thesis: verum