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