let G be _Graph; :: thesis: for W being Walk of G

for e being set st e in W .edges() holds

ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

let W be Walk of G; :: thesis: for e being set st e in W .edges() holds

ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

let e be set ; :: thesis: ( e in W .edges() implies ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) )

reconsider lenW = len W as odd Element of NAT ;

assume e in W .edges() ; :: thesis: ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

then consider n1 being even Element of NAT such that

A1: 1 <= n1 and

A2: n1 <= len W and

A3: W . n1 = e by Lm46;

reconsider n = n1 - 1 as odd Element of NAT by A1, INT_1:5;

set v1 = W . n;

set v2 = W . (n + 2);

n1 - 1 <= (len W) - 0 by A2, XREAL_1:13;

then reconsider v1 = W . n as Vertex of G by Lm1;

n1 < lenW by A2, XXREAL_0:1;

then A4: (n + 1) + 1 <= len W by NAT_1:13;

then reconsider v2 = W . (n + 2) as Vertex of G by Lm1;

take v1 ; :: thesis: ex v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

take v2 ; :: thesis: ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

take n ; :: thesis: ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

thus n + 2 <= len W by A4; :: thesis: ( v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

thus ( v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) ) by A3; :: thesis: e Joins v1,v2,G

(n + 1) - 1 < (len W) - 0 by A2, XREAL_1:15;

hence e Joins v1,v2,G by A3, Def3; :: thesis: verum

for e being set st e in W .edges() holds

ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

let W be Walk of G; :: thesis: for e being set st e in W .edges() holds

ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

let e be set ; :: thesis: ( e in W .edges() implies ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) )

reconsider lenW = len W as odd Element of NAT ;

assume e in W .edges() ; :: thesis: ex v1, v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

then consider n1 being even Element of NAT such that

A1: 1 <= n1 and

A2: n1 <= len W and

A3: W . n1 = e by Lm46;

reconsider n = n1 - 1 as odd Element of NAT by A1, INT_1:5;

set v1 = W . n;

set v2 = W . (n + 2);

n1 - 1 <= (len W) - 0 by A2, XREAL_1:13;

then reconsider v1 = W . n as Vertex of G by Lm1;

n1 < lenW by A2, XXREAL_0:1;

then A4: (n + 1) + 1 <= len W by NAT_1:13;

then reconsider v2 = W . (n + 2) as Vertex of G by Lm1;

take v1 ; :: thesis: ex v2 being Vertex of G ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

take v2 ; :: thesis: ex n being odd Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

take n ; :: thesis: ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

thus n + 2 <= len W by A4; :: thesis: ( v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

thus ( v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) ) by A3; :: thesis: e Joins v1,v2,G

(n + 1) - 1 < (len W) - 0 by A2, XREAL_1:15;

hence e Joins v1,v2,G by A3, Def3; :: thesis: verum