let q be FinSequence; :: thesis: for m, n being Nat
for G being Graph
for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G

let m, n be Nat; :: thesis: for G being Graph
for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G

let G be Graph; :: thesis: for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G

let c be Chain of G; :: thesis: ( 1 <= m & m <= n & n <= len c & q = (m,n) -cut c implies q is Chain of G )
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len c ; :: thesis: ( not q = (m,n) -cut c or q is Chain of G )
A4: m <= n + 1 by ;
consider vs being FinSequence of the carrier of G such that
A5: vs is_vertex_seq_of c by Th33;
set p9 = (m,(n + 1)) -cut vs;
A6: now :: thesis: for k being Nat st 1 <= k & k <= len ((m,(n + 1)) -cut vs) holds
((m,(n + 1)) -cut vs) . k in the carrier of G
let k be Nat; :: thesis: ( 1 <= k & k <= len ((m,(n + 1)) -cut vs) implies ((m,(n + 1)) -cut vs) . k in the carrier of G )
assume that
A7: 1 <= k and
A8: k <= len ((m,(n + 1)) -cut vs) ; :: thesis: ((m,(n + 1)) -cut vs) . k in the carrier of G
k in dom ((m,(n + 1)) -cut vs) by ;
then A9: ((m,(n + 1)) -cut vs) . k in rng ((m,(n + 1)) -cut vs) by FUNCT_1:def 3;
A10: rng vs c= the carrier of G by FINSEQ_1:def 4;
rng ((m,(n + 1)) -cut vs) c= rng vs by FINSEQ_6:137;
hence ((m,(n + 1)) -cut vs) . k in the carrier of G by ; :: thesis: verum
end;
assume A11: q = (m,n) -cut c ; :: thesis: q is Chain of G
then A12: ((len q) + m) - m = (n + 1) - m by A1, A3, A4, Lm2;
A13: len vs = (len c) + 1 by A5;
then A14: n + 1 <= len vs by ;
then A15: ((len ((m,(n + 1)) -cut vs)) + m) - m = ((n + 1) + 1) - m by ;
then A16: len ((m,(n + 1)) -cut vs) = ((n - m) + 1) + 1 ;
A17: now :: thesis: for k being Nat st 1 <= k & k <= len q holds
ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )
1 - 1 <= m - 1 by ;
then m - 1 = m -' 1 by XREAL_0:def 2;
then reconsider m1 = m - 1 as Element of NAT ;
let k be Nat; :: thesis: ( 1 <= k & k <= len q implies ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 ) )

reconsider i = m1 + k as Nat ;
assume that
A18: 1 <= k and
A19: k <= len q ; :: thesis: ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )

0 + 1 <= k by A18;
then consider j being Nat such that
0 <= j and
A20: j < len q and
A21: k = j + 1 by ;
A22: j + 1 < len ((m,(n + 1)) -cut vs) by ;
i + 1 = m + (j + 1) by A21;
then A23: ((m,(n + 1)) -cut vs) . (k + 1) = vs . (i + 1) by ;
set v2 = vs /. (i + 1);
set v1 = vs /. i;
A24: 1 <= i + 1 by NAT_1:12;
A25: i = m + j by A21;
j < len ((m,(n + 1)) -cut vs) by ;
then A26: ((m,(n + 1)) -cut vs) . k = vs . i by ;
i <= (m - 1) + (n - (m - 1)) by ;
then A27: i <= len c by ;
then A28: i <= len vs by ;
take v1 = vs /. i; :: thesis: ex v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )

take v2 = vs /. (i + 1); :: thesis: ( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )
A29: i + 1 <= len vs by ;
1 - 1 <= m - 1 by ;
then A30: 0 + 1 <= (m - 1) + k by ;
then c . i joins v1,v2 by ;
hence ( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 ) by A1, A3, A11, A4, A20, A21, A25, A30, A28, A24, A29, A26, A23, Lm2, FINSEQ_4:15; :: thesis: verum
end;
thus q is Chain of G :: thesis: verum
proof
hereby :: according to GRAPH_1:def 14 :: thesis: ex b1 being set st
( len b1 = (len q) + 1 & ( for b2 being set holds
( not 1 <= b2 or not b2 <= len b1 or b1 . b2 in the carrier of G ) ) & ( for b2 being set holds
( not 1 <= b2 or not b2 <= len q or ex b3, b4 being Element of the carrier of G st
( b3 = b1 . b2 & b4 = b1 . (b2 + 1) & q . b2 joins b3,b4 ) ) ) )
let k be Nat; :: thesis: ( 1 <= k & k <= len q implies q . k in the carrier' of G )
assume that
A31: 1 <= k and
A32: k <= len q ; :: thesis: q . k in the carrier' of G
k in dom q by ;
then A33: q . k in rng q by FUNCT_1:def 3;
rng q c= rng c by ;
then A34: q . k in rng c by A33;
rng c c= the carrier' of G by FINSEQ_1:def 4;
hence q . k in the carrier' of G by A34; :: thesis: verum
end;
take (m,(n + 1)) -cut vs ; :: thesis: ( len ((m,(n + 1)) -cut vs) = (len q) + 1 & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b1 in the carrier of G ) ) & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) ) ) )

thus len ((m,(n + 1)) -cut vs) = (len q) + 1 by ; :: thesis: ( ( for b1 being set holds
( not 1 <= b1 or not b1 <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b1 in the carrier of G ) ) & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) ) ) )

thus for n being Nat st 1 <= n & n <= len ((m,(n + 1)) -cut vs) holds
((m,(n + 1)) -cut vs) . n in the carrier of G by A6; :: thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) )

thus for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) ) by A17; :: thesis: verum
end;