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 ;
set v1 = W . n;
set v2 = W . (n + 2);
n1 - 1 <= (len W) - 0 by ;
then reconsider v1 = W . n as Vertex of G by Lm1;
n1 < lenW by ;
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 ;
hence e Joins v1,v2,G by ; :: thesis: verum