hereby :: thesis: ( not v in W .vertices() implies ex b1 being odd Element of NAT st b1 = len W )
defpred S1[ Nat] means ( \$1 is odd & \$1 <= len W & W . \$1 = v );
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 ) )

then A2: W . (W .find v) = v by Def19;
W .find v <= len W by ;
then A3: ex k being Nat st S1[k] by A2;
A4: for k being Nat st S1[k] holds
k <= len W ;
consider IT being Nat such that
A5: ( S1[IT] & ( for n being Nat st S1[n] holds
n <= IT ) ) from NAT_1:sch 6(A4, A3);
reconsider IT = IT as odd Element of NAT by ;
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 A5; :: 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 that
A6: n <= len W and
A7: W . n = v ; :: thesis: n <= IT
thus n <= IT by A5, A6, A7; :: thesis: verum
end;
thus ( not v in W .vertices() implies ex b1 being odd Element of NAT st b1 = len W ) ; :: thesis: verum