theorem :: MSSCYC_1:13

for m, n being Nat
for G being non void Graph
for c, c1 being directed Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c holds
vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)