let G be _Graph; :: thesis: for W being Trail of G
for v being Vertex of G st v in W .vertices() & v is endvertex & not v = W .first() holds
v = W .last()

let W be Trail of G; :: thesis: for v being Vertex of G st v in W .vertices() & v is endvertex & not v = W .first() holds
v = W .last()

let v be Vertex of G; :: thesis: ( v in W .vertices() & v is endvertex & not v = W .first() implies v = W .last() )
assume that
A1: v in W .vertices() and
A2: v is endvertex ; :: thesis: ( v = W .first() or v = W .last() )
consider e being object such that
A3: v .edgesInOut() = {e} and
not e Joins v,v,G by ;
consider n being odd Element of NAT such that
A4: n <= len W and
A5: W . n = v by ;
A6: W .vertexAt n = v by A4, A5, Def8;
now :: thesis: ( v <> W .first() implies not v <> W .last() )
reconsider naa1 = n - 1 as even Element of NAT by ;
assume that
A7: v <> W .first() and
A8: v <> W .last() ; :: thesis: contradiction
A9: n - 1 < naa1 + 2 by NAT_1:16;
1 <= n by ABIAN:12;
then A10: 1 < n by ;
then 1 + 1 <= n by NAT_1:13;
then A11: (1 + 1) - 1 <= n - 1 by XREAL_1:13;
A12: n < len W by ;
then A13: W . (n + 1) in v .edgesInOut() by ;
W . (n - 1) in v .edgesInOut() by A4, A6, A10, Th10;
then A14: W . (n - 1) = e by ;
n + 1 <= len W by ;
then W . naa1 <> W . (n + 1) by ;
hence contradiction by A3, A14, A13, TARSKI:def 1; :: thesis: verum
end;
hence ( v = W .first() or v = W .last() ) ; :: thesis: verum