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 Nat st n <= len W & W . n = v holds
IT <= n ) )
set vs = W .vertexSeq() ;
defpred S₁[ Nat] means ( not $1 is even & $1 <= len W & W . $1 = v );

now

consider i being Nat such that
A2: ( i in dom (W .vertexSeq() ) & (W .vertexSeq() ) . i = v ) by A1, FINSEQ_2:11;
set n1 = 2 * i;
reconsider n1 = 2 * i as even Nat ;
set n = n1 - 1;
A3: ( 1 <= i & i <= len (W .vertexSeq() ) ) by A2, FINSEQ_3:27;
then 1 <= i + i by NAT_1:12;
then reconsider n = n1 - 1 as odd Element of NAT by INT_1:18;
take n = n; :: thesis: ( n <= len W & W . n = v )
i * 2 <= (len (W .vertexSeq() )) * 2 by A3, XREAL_1:66;
then i * 2 <= (len W) + 1 by Def14;
then n1 - 1 <= ((len W) + 1) - 1 by XREAL_1:15;
hence n <= len W ; :: thesis: W . n = v
thus W . n = v by A2, A3, Def14; :: thesis: verum

end;

then A4: ex k being Nat st S₁[k] ;
consider IT being Nat such that
A5: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(A4);
reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 13;
take IT = IT; :: thesis: ( IT <= len W & W . IT = v & ( for n being odd Nat st n <= len W & W . n = v holds
IT <= n ) )
thus ( IT <= len W & W . IT = v ) by A5; :: thesis: for n being odd Nat st n <= len W & W . n = v holds
IT <= n
let n be odd Nat; :: thesis: ( n <= len W & W . n = v implies IT <= n )
assume ( n <= len W & W . n = v ) ; :: thesis: IT <= n
hence IT <= n by A5; :: thesis: verum

end;

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