let G be _Graph; for W being Walk of G
for u, e, v being object st e Joins u,v,G & e in W .edges() & not G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
G .walkOf (v,e,u) is_odd_substring_of W, 0
let W be Walk of G; for u, e, v being object st e Joins u,v,G & e in W .edges() & not G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
G .walkOf (v,e,u) is_odd_substring_of W, 0
let u, e, v be object ; ( e Joins u,v,G & e in W .edges() & not G .walkOf (u,e,v) is_odd_substring_of W, 0 implies G .walkOf (v,e,u) is_odd_substring_of W, 0 )
assume that
A1:
e Joins u,v,G
and
A2:
e in W .edges()
; ( G .walkOf (u,e,v) is_odd_substring_of W, 0 or G .walkOf (v,e,u) is_odd_substring_of W, 0 )
consider n being odd Element of NAT such that
A3:
( n < len W & W . (n + 1) = e )
by A2, GLIB_001:100;
n + 2 <= len W
by A3, GLIB_001:1;
then A4:
G .walkOf ((W . n),e,(W . (n + 2))) is_odd_substring_of W, 0
by A3, Th31;
e Joins W . n,W . (n + 2),G
by A3, GLIB_001:def 3;