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;

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() )

hence
( v = W .first() or v = W .last() )
; :: thesis: verumreconsider 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;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