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

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