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 A2, NAT_1:12;

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;

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 A3, XREAL_1:6;

then A15: ((len ((m,(n + 1)) -cut vs)) + m) - m = ((n + 1) + 1) - m by A1, A4, FINSEQ_6:def 4;

then A16: len ((m,(n + 1)) -cut vs) = ((n - m) + 1) + 1 ;

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 A2, NAT_1:12;

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

assume A11:
q = (m,n) -cut c
; :: thesis: q is Chain of G((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 A7, A8, FINSEQ_3:25;

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 A10, A9; :: thesis: verum

end;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 A7, A8, FINSEQ_3:25;

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 A10, A9; :: thesis: verum

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 A3, XREAL_1:6;

then A15: ((len ((m,(n + 1)) -cut vs)) + m) - m = ((n + 1) + 1) - m by A1, A4, FINSEQ_6:def 4;

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 )

thus
q is Chain of G
:: thesis: verumex 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 A1, XREAL_1:9;

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 A19, FINSEQ_6:127;

A22: j + 1 < len ((m,(n + 1)) -cut vs) by A12, A16, A20, XREAL_1:6;

i + 1 = m + (j + 1) by A21;

then A23: ((m,(n + 1)) -cut vs) . (k + 1) = vs . (i + 1) by A1, A4, A14, A22, FINSEQ_6:def 4;

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 A12, A16, A20, NAT_1:13;

then A26: ((m,(n + 1)) -cut vs) . k = vs . i by A1, A4, A14, A25, A22, FINSEQ_6:def 4;

i <= (m - 1) + (n - (m - 1)) by A12, A19, XREAL_1:6;

then A27: i <= len c by A3, XXREAL_0:2;

then A28: i <= len vs by A13, NAT_1:12;

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 A13, A27, XREAL_1:7;

1 - 1 <= m - 1 by A1, XREAL_1:9;

then A30: 0 + 1 <= (m - 1) + k by A18, XREAL_1:7;

then c . i joins v1,v2 by A5, A27;

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;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 A19, FINSEQ_6:127;

A22: j + 1 < len ((m,(n + 1)) -cut vs) by A12, A16, A20, XREAL_1:6;

i + 1 = m + (j + 1) by A21;

then A23: ((m,(n + 1)) -cut vs) . (k + 1) = vs . (i + 1) by A1, A4, A14, A22, FINSEQ_6:def 4;

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 A12, A16, A20, NAT_1:13;

then A26: ((m,(n + 1)) -cut vs) . k = vs . i by A1, A4, A14, A25, A22, FINSEQ_6:def 4;

i <= (m - 1) + (n - (m - 1)) by A12, A19, XREAL_1:6;

then A27: i <= len c by A3, XXREAL_0:2;

then A28: i <= len vs by A13, NAT_1:12;

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 A13, A27, XREAL_1:7;

1 - 1 <= m - 1 by A1, XREAL_1:9;

then A30: 0 + 1 <= (m - 1) + k by A18, XREAL_1:7;

then c . i joins v1,v2 by A5, A27;

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

proof
_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b_{1} in the carrier of G ) ) & ( for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len q or ex b_{2}, b_{3} being Element of the carrier of G st

( b_{2} = ((m,(n + 1)) -cut vs) . b_{1} & b_{3} = ((m,(n + 1)) -cut vs) . (b_{1} + 1) & q . b_{1} joins b_{2},b_{3} ) ) ) )

thus len ((m,(n + 1)) -cut vs) = (len q) + 1 by A12, A15; :: thesis: ( ( for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b_{1} in the carrier of G ) ) & ( for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len q or ex b_{2}, b_{3} being Element of the carrier of G st

( b_{2} = ((m,(n + 1)) -cut vs) . b_{1} & b_{3} = ((m,(n + 1)) -cut vs) . (b_{1} + 1) & q . b_{1} joins b_{2},b_{3} ) ) ) )

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 b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len q or ex b_{2}, b_{3} being Element of the carrier of G st

( b_{2} = ((m,(n + 1)) -cut vs) . b_{1} & b_{3} = ((m,(n + 1)) -cut vs) . (b_{1} + 1) & q . b_{1} joins b_{2},b_{3} ) )

thus for b_{1} being set holds

( not 1 <= b_{1} or not b_{1} <= len q or ex b_{2}, b_{3} being Element of the carrier of G st

( b_{2} = ((m,(n + 1)) -cut vs) . b_{1} & b_{3} = ((m,(n + 1)) -cut vs) . (b_{1} + 1) & q . b_{1} joins b_{2},b_{3} ) )
by A17; :: thesis: verum

end;

hereby :: according to GRAPH_1:def 14 :: thesis: ex b_{1} being set st

( len b_{1} = (len q) + 1 & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len b_{1} or b_{1} . b_{2} in the carrier of G ) ) & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len q or ex b_{3}, b_{4} being Element of the carrier of G st

( b_{3} = b_{1} . b_{2} & b_{4} = b_{1} . (b_{2} + 1) & q . b_{2} joins b_{3},b_{4} ) ) ) )

take
(m,(n + 1)) -cut vs
; :: thesis: ( len ((m,(n + 1)) -cut vs) = (len q) + 1 & ( for b( len b

( not 1 <= b

( not 1 <= b

( b

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 A31, A32, FINSEQ_3:25;

then A33: q . k in rng q by FUNCT_1:def 3;

rng q c= rng c by A11, FINSEQ_6:137;

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;assume that

A31: 1 <= k and

A32: k <= len q ; :: thesis: q . k in the carrier' of G

k in dom q by A31, A32, FINSEQ_3:25;

then A33: q . k in rng q by FUNCT_1:def 3;

rng q c= rng c by A11, FINSEQ_6:137;

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

( not 1 <= b

( not 1 <= b

( b

thus len ((m,(n + 1)) -cut vs) = (len q) + 1 by A12, A15; :: thesis: ( ( for b

( not 1 <= b

( not 1 <= b

( b

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 b

( not 1 <= b

( b

thus for b

( not 1 <= b

( b