let G be _Graph; :: thesis: for W being Walk of G
for e, x, y being set 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; :: thesis: for e, x, y being set st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() )
let e, x, y be set ; :: thesis: ( e in W .edges() & e Joins x,y,G implies ( x in W .vertices() & y in W .vertices() ) )
assume A1: ( e in W .edges() & e Joins x,y,G ) ; :: thesis: ( x in W .vertices() & y in W .vertices() )
then consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A2: ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) by Lm47;
A3: v2 in W .vertices() by A2, Lm45;
(n + 2) - 2 <= (len W) - 0 by A2, XREAL_1:15;
then v1 in W .vertices() by A2, Lm45;
hence ( x in W .vertices() & y in W .vertices() ) by A1, A2, A3, GLIB_000:18; :: thesis: verum