let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum