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 A2, GLIB_000:def 51;
consider n being odd Element of NAT such that
A4: n <= len W and
A5: W . n = v by A1, Lm45;
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 ABIAN:12, INT_1:5;
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 A5, A7, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then A11: (1 + 1) - 1 <= n - 1 by XREAL_1:13;
A12: n < len W by A4, A5, A8, XXREAL_0:1;
then A13: W . (n + 1) in v .edgesInOut() by A6, Th9;
W . (n - 1) in v .edgesInOut() by A4, A6, A10, Th10;
then A14: W . (n - 1) = e by A3, TARSKI:def 1;
n + 1 <= len W by A12, NAT_1:13;
then W . naa1 <> W . (n + 1) by A11, A9, Lm57;
hence contradiction by A3, A14, A13, TARSKI:def 1; :: thesis: verum

end;

hence ( v = W .first() or v = W .last() ) ; :: thesis: verum