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 that
A1: W is_Walk_from x,y and
A2: e Joins y,z,G ; :: thesis: W .addEdge e is_Walk_from x,z
A3: W .last() = y by A1, Def23;
W .first() = x by A1, Def23;
hence W .addEdge e is_Walk_from x,z by A2, A3, Lm36; :: thesis: verum