hereby :: thesis: ( ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) & ( for b_{1} being Vertex of G holds verum ) )

thus
( ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) & ( for breconsider n1 = n as Element of NAT by ORDINAL1:def 12;

assume that

A1: n is odd and

A2: n <= len W ; :: thesis: W . n is Vertex of G

end;assume that

A1: n is odd and

A2: n <= len W ; :: thesis: W . n is Vertex of G

now :: thesis: W . n is Vertex of Gend;

hence
W . n is Vertex of G
; :: thesis: verum