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