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 );
set vs = W .vertexSeq() ;
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 ) )

now :: thesis: ex n being odd Element of NAT st
( n <= len W & W . n = v )

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

end;

then A6: ex k being Nat st S₁[k] ;
consider IT being Nat such that
A7: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(A6);
reconsider IT = IT as odd Element of NAT by A7, ORDINAL1:def 12;
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 A7; :: 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 that
A8: n <= len W and
A9: W . n = v ; :: thesis: IT <= n
thus IT <= n by A7, A8, A9; :: thesis: verum

end;

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