let G be _Graph; for W being Walk of G
for e, x, y being object st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() )
let W be Walk of G; for e, x, y being object st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() )
let e, x, y be object ; ( e in W .edges() & e Joins x,y,G implies ( x in W .vertices() & y in W .vertices() ) )
assume that
A1:
e in W .edges()
and
A2:
e Joins x,y,G
; ( x in W .vertices() & y in W .vertices() )
consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A3:
n + 2 <= len W
and
A4:
v1 = W . n
and
e = W . (n + 1)
and
A5:
v2 = W . (n + 2)
and
A6:
e Joins v1,v2,G
by A1, Lm47;
(n + 2) - 2 <= (len W) - 0
by A3, XREAL_1:13;
then A7:
v1 in W .vertices()
by A4, Lm45;
v2 in W .vertices()
by A3, A5, Lm45;
hence
( x in W .vertices() & y in W .vertices() )
by A2, A6, A7, GLIB_000:15; verum