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 )

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 S₁[n] by A1, A2;
consider IT being Nat such that
A4: ( S₁[IT] & ( for k being Nat st S₁[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 b₁ being odd Element of NAT st b₁ = len W ) ; :: thesis: verum