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 ) )
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 & n1 <= len W & W . n1 = e ) by Lm46;
reconsider n = n1 - 1 as odd Element of NAT by A1, INT_1:18;
set v1 = W . n;
set v2 = W . (n + 2);
n1 - 1 <= (len W) - 0 by A1, XREAL_1:15;
then reconsider v1 = W . n as Vertex of G by Lm1;
reconsider lenW = len W as odd Element of NAT ;
n1 < lenW by A1, XXREAL_0:1;
then A2: (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 A2; :: 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 A1; :: thesis: e Joins v1,v2,G
(n + 1) - 1 < (len W) - 0 by A1, XREAL_1:17;
hence e Joins v1,v2,G by A1, Def3; :: thesis: verum