hereby :: thesis: ( ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) & ( for b1 being Vertex of G holds verum ) )
reconsider 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
now :: thesis: W . n is Vertex of G
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 ( ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) & ( for b1 being Vertex of G holds verum ) ) ; :: thesis: verum