let G be _Graph; :: thesis: for W being Walk of G

for m, n being odd Element of NAT

for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT

for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let m, n be odd Element of NAT ; :: thesis: for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let x be Element of NAT ; :: thesis: ( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

assume A1: x in dom (W .remove (m,n)) ; :: thesis: ( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

1 <= x by A1, FINSEQ_3:25;

hence ( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) ) by A1, FINSEQ_1:1, FINSEQ_3:25; :: thesis: verum

for m, n being odd Element of NAT

for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT

for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let m, n be odd Element of NAT ; :: thesis: for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

let x be Element of NAT ; :: thesis: ( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

assume A1: x in dom (W .remove (m,n)) ; :: thesis: ( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

1 <= x by A1, FINSEQ_3:25;

hence ( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) ) by A1, FINSEQ_1:1, FINSEQ_3:25; :: thesis: verum