let G be _Graph; :: thesis: for W being Walk of G
for e, x, y, z being set st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z
let W be Walk of G; :: thesis: for e, x, y, z being set st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z
let e, x, y, z be set ; :: thesis: ( W is_Walk_from x,y & e Joins y,z,G implies W .addEdge e is_Walk_from x,z )
assume A1: ( W is_Walk_from x,y & e Joins y,z,G ) ; :: thesis: W .addEdge e is_Walk_from x,z
then ( W .first() = x & W .last() = y ) by Def23;
hence W .addEdge e is_Walk_from x,z by A1, Lm36; :: thesis: verum