hereby :: thesis: ( not v in W .vertices() implies ex b₁ being odd Element of NAT st b₁ = len W )

assume A1: v in W .vertices() ; :: thesis: ex IT being odd Element of NAT st
( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT ) )
defpred S₁[ Nat] means ( not $1 is even & $1 <= len W & W . $1 = v );
A2: for k being Nat st S₁[k] holds
k <= len W ;
( W .find v <= len W & W . (W .find v) = v ) by A1, Def19;
then A3: ex k being Nat st S₁[k] ;
consider IT being Nat such that
A4: ( S₁[IT] & ( for n being Nat st S₁[n] holds
n <= IT ) ) from NAT_1:sch 6(A2, A3);
reconsider IT = IT as odd Element of NAT by A4, ORDINAL1:def 13;
take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT ) )
thus ( IT <= len W & W . IT = v ) by A4; :: thesis: for n being odd Element of NAT st n <= len W & W . n = v holds
n <= IT
let n be odd Element of NAT ; :: thesis: ( n <= len W & W . n = v implies n <= IT )
assume ( n <= len W & W . n = v ) ; :: thesis: n <= IT
hence n <= IT by A4; :: thesis: verum

end;

thus ( not v in W .vertices() implies ex b₁ being odd Element of NAT st b₁ = len W ) ; :: thesis: verum