for G being _Graph
for W1, W2 being Walk of G
for x, y, z being object st W1 is_Walk_from x,y & W2 is_Walk_from y,z holds
W1 .append W2 is_Walk_from x,z by Lm11;