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:27;
hence ( x in Seg m or ( m <= x & x <= len (W .remove m,n) ) ) by A1, FINSEQ_1:3, FINSEQ_3:27; :: thesis: verum