:: deftheorem Def12 defines .remove GLIB_001:def 12 :
for G being _Graph
for W being Walk of G
for m, n being Element of NAT holds
( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W .remove (m,n) = W ) );