let G be _Graph; :: thesis: for W being Walk of G
for m, n being odd Element of NAT st m <= n & n < len W holds
(W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2)
let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n < len W holds
(W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2)
let m, n be odd Element of NAT ; :: thesis: ( m <= n & n < len W implies (W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2) )
set W1 = W .cut m,n;
set e = W . (n + 1);
assume A1: ( m <= n & n < len W ) ; :: thesis: (W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2)
then A2: ( n <= n + 2 & n + 2 <= len W ) by Th1;
A3: (W .cut m,n) .last() = W . n by A1, Lm16;
then W . (n + 1) Joins (W .cut m,n) .last() ,W . (n + 2),G by A1, Def3;
then W . (n + 1) Joins (W .cut m,n) .last() ,W .vertexAt (n + 2),G by A2, Def8;
then ((W .cut m,n) .last() ) .adj (W . (n + 1)) = W .vertexAt (n + 2) by GLIB_000:69;
then ((W .cut m,n) .last() ) .adj (W . (n + 1)) = W . (n + 2) by A2, Def8;
then G .walkOf ((W .cut m,n) .last() ),(W . (n + 1)),(((W .cut m,n) .last() ) .adj (W . (n + 1))) = W .cut n,(n + 2) by A1, A3, Th41;
hence (W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2) by A1, A2, Lm17; :: thesis: verum