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)) .vertices() c= W .vertices()

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)) .vertices() c= W .vertices()

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies (W .cut (m,n)) .vertices() c= W .vertices() )

set W2 = W .cut (m,n);

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: (W .cut (m,n)) .vertices() c= W .vertices()

for m, n being odd Element of NAT st m <= n & n <= len W holds

(W .cut (m,n)) .vertices() c= W .vertices()

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)) .vertices() c= W .vertices()

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies (W .cut (m,n)) .vertices() c= W .vertices() )

set W2 = W .cut (m,n);

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: (W .cut (m,n)) .vertices() c= W .vertices()

now :: thesis: for x being object st x in (W .cut (m,n)) .vertices() holds

x in W .vertices()

hence
(W .cut (m,n)) .vertices() c= W .vertices()
by TARSKI:def 3; :: thesis: verumx in W .vertices()

let x be object ; :: thesis: ( x in (W .cut (m,n)) .vertices() implies x in W .vertices() )

assume x in (W .cut (m,n)) .vertices() ; :: thesis: x in W .vertices()

then consider n being odd Element of NAT such that

A3: n <= len (W .cut (m,n)) and

A4: (W .cut (m,n)) . n = x by Lm45;

reconsider naa1 = n - 1 as even Element of NAT by ABIAN:12, INT_1:5;

A5: naa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

then m + naa1 in dom W by A1, A2, Lm15;

then A6: m + naa1 <= len W by FINSEQ_3:25;

(W .cut (m,n)) . (naa1 + 1) = W . (m + naa1) by A1, A2, A5, Lm15;

hence x in W .vertices() by A4, A6, Lm45; :: thesis: verum

end;assume x in (W .cut (m,n)) .vertices() ; :: thesis: x in W .vertices()

then consider n being odd Element of NAT such that

A3: n <= len (W .cut (m,n)) and

A4: (W .cut (m,n)) . n = x by Lm45;

reconsider naa1 = n - 1 as even Element of NAT by ABIAN:12, INT_1:5;

A5: naa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

then m + naa1 in dom W by A1, A2, Lm15;

then A6: m + naa1 <= len W by FINSEQ_3:25;

(W .cut (m,n)) . (naa1 + 1) = W . (m + naa1) by A1, A2, A5, Lm15;

hence x in W .vertices() by A4, A6, Lm45; :: thesis: verum