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 );
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 () and
A3: (W .vertexSeq()) . i = v by ;
set n1 = 2 * i;
reconsider n1 = 2 * i as even Nat ;
set n = n1 - 1;
A4: 1 <= i by ;
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 () by ;
then i * 2 <= (len ()) * 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 S1[k] ;
consider IT being Nat such that
A7: ( S1[IT] & ( for n being Nat st S1[n] holds
IT <= n ) ) from reconsider IT = IT as odd Element of NAT by ;
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 b1 being odd Element of NAT st b1 = len W
take len W ; :: thesis: len W = len W
thus len W = len W ; :: thesis: verum