theorem Th42: :: GRAPH_2:42

for m, n being Nat
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_vertex_seq_of c1