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 for x being object st x in (W .cut (m,n)) .vertices() holds
x in W .vertices() let x be
object ;
( 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: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;
verum end;
hence
(W .cut (m,n)) .vertices() c= W .vertices()
by TARSKI:def 3; verum