let m, n be Element of NAT ; :: thesis: 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)
let G be non void Graph; :: thesis: 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)
let c, c1 be directed Chain of G; :: thesis: ( 1 <= m & m <= n & n <= len c & c1 = m,n -cut c implies vertex-seq c1 = m,(n + 1) -cut (vertex-seq c) )
assume A1: ( 1 <= m & m <= n & n <= len c & c1 = m,n -cut c ) ; :: thesis: vertex-seq c1 = m,(n + 1) -cut (vertex-seq c)
set mn1c = m,(n + 1) -cut (vertex-seq c);
set vsc = vertex-seq c;
A2: not c is empty by A1;
then A3: vertex-seq c is_vertex_seq_of c by GRAPH_2:def 11;
then A4: m,(n + 1) -cut (vertex-seq c) is_vertex_seq_of c1 by A1, GRAPH_2:45;
A5: not c1 is empty by A1, A2, Th12;
then A6: len c1 <> 0 ;
A7: m <= len c by A1, XXREAL_0:2;
A8: ( m <= n + 1 & 0 < len c1 ) by A1, A6, NAT_1:12;
then A9: c1 . (0 + 1) = c . (m + 0 ) by A1, GRAPH_2:def 1;
A10: len (vertex-seq c) = (len c) + 1 by A3, GRAPH_2:def 7;
then A11: n + 1 <= len (vertex-seq c) by A1, XREAL_1:8;
not vertex-seq c is empty by A10;
then not m,(n + 1) -cut (vertex-seq c) is empty by A1, A8, A11, Th12;
then len (m,(n + 1) -cut (vertex-seq c)) <> 0 ;
then ( 0 < len (m,(n + 1) -cut (vertex-seq c)) & m <= n + 1 ) by A1, NAT_1:12;
then (vertex-seq c) . (m + 0 ) = (m,(n + 1) -cut (vertex-seq c)) . (0 + 1) by A1, A11, GRAPH_2:def 1;
then (m,(n + 1) -cut (vertex-seq c)) . 1 = the Source of G . (c1 . 1) by A1, A2, A7, A9, Th11;
hence vertex-seq c1 = m,(n + 1) -cut (vertex-seq c) by A4, A5, GRAPH_2:def 11; :: thesis: verum