theorem :: MSSCYC_1:9

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