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