hereby :: thesis: ( ( ( n is even or not n <= len W ) implies W .first() is Vertex of G ) & ( for b₁ being Vertex of G holds verum ) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume that
A1: not n is even and
A2: n <= len W ; :: thesis: W . n is Vertex of G

now

per cases ( n = len W or n <> len W ) ;

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

then W . n = W .last() ;
hence W . n is Vertex of G ; :: thesis: verum

end;

suppose n <> len W ; :: thesis: W . n is Vertex of G

then n < len W by A2, XXREAL_0:1;
then W . (n1 + 1) Joins W . n,W . (n + 2),G by A1, Def3;
hence W . n is Vertex of G by GLIB_000:13; :: thesis: verum

end;

end;

end;

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

end;

thus ( ( ( n is even or not n <= len W ) implies W .first() is Vertex of G ) & ( for b₁ being Vertex of G holds verum ) ) ; :: thesis: verum