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 A1:
( v in W .vertices() & v is endvertex )
; :: thesis: ( v = W .first() or v = W .last() )
then consider n being odd Element of NAT such that
A2:
( n <= len W & W . n = v )
by Lm45;
A3:
W .vertexAt n = v
by A2, Def8;
consider e being set such that
A4:
( v .edgesInOut() = {e} & not e Joins v,v,G )
by A1, GLIB_000:def 53;
now assume A5:
(
v <> W .first() &
v <> W .last() )
;
:: thesis: contradiction
1
<= n
by HEYTING3:1;
then A6:
1
< n
by A2, A5, XXREAL_0:1;
reconsider naa1 =
n - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
1
+ 1
<= n
by A6, NAT_1:13;
then A7:
(1 + 1) - 1
<= n - 1
by XREAL_1:15;
A8:
n < len W
by A2, A5, XXREAL_0:1;
then A9:
n + 1
<= len W
by NAT_1:13;
n - 1
< naa1 + 2
by NAT_1:16;
then A10:
W . naa1 <> W . (n + 1)
by A7, A9, Lm57;
W . (n - 1) in v .edgesInOut()
by A2, A3, A6, Th12;
then A11:
W . (n - 1) = e
by A4, TARSKI:def 1;
W . (n + 1) in v .edgesInOut()
by A3, A8, Th11;
hence
contradiction
by A4, A10, A11, TARSKI:def 1;
:: thesis: verum end;
hence
( v = W .first() or v = W .last() )
; :: thesis: verum