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