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

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

now

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

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

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

end;

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

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 by GLIB_000:16; :: thesis: verum

end;

end;

end;

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

end;

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