let G be _Graph; 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; 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 ; ( 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 that
A1:
m <= n
and
A2:
n < len W
; (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))
A3:
n + 2 <= len W
by A2, Th1;
A4:
(W .cut (m,n)) .last() = W . n
by A1, A2, Lm16;
then
W . (n + 1) Joins (W .cut (m,n)) .last() ,W . (n + 2),G
by A2, Def3;
then
W . (n + 1) Joins (W .cut (m,n)) .last() ,W .vertexAt (n + 2),G
by A3, Def8;
then
((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W .vertexAt (n + 2)
by GLIB_000:66;
then
((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W . (n + 2)
by A3, Def8;
then A5:
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 A2, A4, Th38;
n <= n + 2
by Th1;
hence
(W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))
by A1, A3, A5, Lm17; verum