defpred S₁[ Nat] means ( $1 is odd & $1 <= len W & W . $1 = v );
set vs = W .vertexSeq() ;
assume A1: v in W .vertices() ; :: thesis:

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:
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:
thus W . n = v by A3, A4, A5, Def14; :: thesis:

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:
thus ( IT <= len W & W . IT = v ) by A7; :: thesis:
let n be odd Nat; :: thesis:
assume that
A8: n <= len W and
A9: W . n = v ; :: thesis:
thus IT <= n by A7, A8, A9; :: thesis:

end;