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) .vertices() c= W .vertices()
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) .vertices() c= W .vertices()
let m, n be odd Element of NAT ; ( 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
; (W .cut m,n) .vertices() c= W .vertices()
now let x be
set ;
( x in (W .cut m,n) .vertices() implies x in W .vertices() )assume
x in (W .cut m,n) .vertices()
;
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:18;
A5:
naa1 < (len (W .cut m,n)) - 0
by A3, XREAL_1:17;
then
m + naa1 in dom W
by A1, A2, Lm15;
then A6:
m + naa1 <= len W
by FINSEQ_3:27;
(W .cut m,n) . (naa1 + 1) = W . (m + naa1)
by A1, A2, A5, Lm15;
hence
x in W .vertices()
by A4, A6, Lm45;
verum end;
hence
(W .cut m,n) .vertices() c= W .vertices()
by TARSKI:def 3; verum