let q be FinSequence; :: thesis: for m, n being Element of 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 Element of 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 )
assume A4:
q = m,n -cut c
; :: thesis: q is Chain of G
consider vs being FinSequence of the carrier of G such that
A5:
vs is_vertex_seq_of c
by Th36;
set p' = m,(n + 1) -cut vs;
A6:
len vs = (len c) + 1
by A5, Def7;
then A7:
( m <= n + 1 & n + 1 <= len vs )
by A2, A3, NAT_1:12, XREAL_1:8;
then A8:
((len q) + m) - m = (n + 1) - m
by A1, A3, A4, Lm2;
A9:
((len (m,(n + 1) -cut vs)) + m) - m = ((n + 1) + 1) - m
by A1, A7, Def1;
then A10:
len (m,(n + 1) -cut vs) = ((n - m) + 1) + 1
;
A11:
now let k be
Element of
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 A12:
1
<= k
and A13:
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 A12, A13, FINSEQ_3:27;
then A14:
(m,(n + 1) -cut vs) . k in rng (m,(n + 1) -cut vs)
by FUNCT_1:def 5;
rng (m,(n + 1) -cut vs) c= rng vs
by Th11;
then A15:
(m,(n + 1) -cut vs) . k in rng vs
by A14;
rng vs c= the
carrier of
G
by FINSEQ_1:def 4;
hence
(m,(n + 1) -cut vs) . k in the
carrier of
G
by A15;
:: thesis: verum end;
A16:
now let k be
Element of
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 ) )
1
- 1
<= m - 1
by A1, XREAL_1:11;
then
m - 1
= m -' 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
reconsider i =
m1 + k as
Element of
NAT ;
assume that A17:
1
<= k
and A18:
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 A17;
then consider j being
Element of
NAT such that A19:
(
0 <= j &
j < len q &
k = j + 1 )
by A18, Th1;
A20:
i = m + j
by A19;
set v1 =
vs /. i;
set v2 =
vs /. (i + 1);
1
- 1
<= m - 1
by A1, XREAL_1:11;
then A21:
0 + 1
<= (m - 1) + k
by A17, XREAL_1:9;
i <= (m - 1) + (n - (m - 1))
by A8, A18, XREAL_1:8;
then A22:
( 1
<= i &
i <= len c )
by A3, A21, XXREAL_0:2;
then A23:
c . i joins vs /. i,
vs /. (i + 1)
by A5, Def7;
A24:
(
i <= len vs & 1
<= i + 1 &
i + 1
<= len vs )
by A6, A22, NAT_1:12, XREAL_1:9;
A25:
i + 1
= m + (j + 1)
by A19;
(
j < len (m,(n + 1) -cut vs) &
j + 1
< len (m,(n + 1) -cut vs) )
by A8, A10, A19, NAT_1:13, XREAL_1:8;
then A26:
(
(m,(n + 1) -cut vs) . k = vs . i &
(m,(n + 1) -cut vs) . (k + 1) = vs . (i + 1) )
by A1, A7, A20, A25, Def1;
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 )thus
(
v1 = (m,(n + 1) -cut vs) . k &
v2 = (m,(n + 1) -cut vs) . (k + 1) &
q . k joins v1,
v2 )
by A1, A3, A4, A7, A19, A20, A21, A23, A24, A26, Lm2, FINSEQ_4:24;
:: thesis: verum end;
thus
q is Chain of G
:: thesis: verumproof
take
m,
(n + 1) -cut vs
;
:: thesis: ( len (m,(n + 1) -cut vs) = (len q) + 1 & ( for b1 being Element of NAT 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 Element of NAT 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 A8, A9;
:: thesis: ( ( for b1 being Element of NAT 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 Element of NAT 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
Element of
NAT st 1
<= n &
n <= len (m,(n + 1) -cut vs) holds
(m,(n + 1) -cut vs) . n in the
carrier of
G
by A11;
:: thesis: for b1 being Element of NAT 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
Element of
NAT 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 A16;
:: thesis: verum
end;