let G be _Graph; :: thesis:
let W be Walk of G; :: thesis:
let u, e, v be object ; :: thesis:
assume that
A1: e Joins u,v,G and
A2: e in W .edges() ; :: thesis:
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;

end;

end;