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()

now :: thesis: for x being object st x in (W .cut (m,n)) .vertices() holds
x 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;

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