:: deftheorem Def11 defines .cut GLIB_001:def 11 :
for G being _Graph
for W being Walk of G
for m, n being Nat holds
( ( m is odd & n is odd & m <= n & n <= len W implies W .cut (m,n) = (m,n) -cut W ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W .cut (m,n) = W ) );