let m, n be Element of NAT ; for G being non void Graph
for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds
m,n -cut c is directed Chain of G
let G be non void Graph; for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds
m,n -cut c is directed Chain of G
let c be directed Chain of G; ( 1 <= m & m <= n & n <= len c implies m,n -cut c is directed Chain of G )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
; m,n -cut c is directed Chain of G
reconsider mnc = m,n -cut c as Chain of G by A1, A2, A3, GRAPH_2:44;
A4:
(len mnc) + m = n + 1
by A1, A2, A3, GRAPH_2:def 1;
now A5:
(len mnc) + m <= (len c) + 1
by A3, A4, XREAL_1:8;
let k be
Element of
NAT ;
( 1 <= k & k < len mnc implies the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k) )assume that A6:
1
<= k
and A7:
k < len mnc
;
the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k)
0 + 1
<= k
by A6;
then consider i being
Element of
NAT such that
0 <= i
and A8:
i < len mnc
and A9:
k = i + 1
by A7, GRAPH_2:1;
A10:
1
<= m + i
by A1, NAT_1:12;
m + (i + 1) < (len mnc) + m
by A7, A9, XREAL_1:8;
then
(m + i) + 1
< (len c) + 1
by A5, XXREAL_0:2;
then A11:
m + i < len c
by XREAL_1:8;
A12:
mnc . (k + 1) = c . (m + k)
by A1, A2, A3, A7, GRAPH_2:def 1;
(
mnc . (i + 1) = c . (m + i) &
m + k = (m + i) + 1 )
by A1, A2, A3, A8, A9, GRAPH_2:def 1;
hence
the
Source of
G . (mnc . (k + 1)) = the
Target of
G . (mnc . k)
by A12, A10, A11, GRAPH_1:def 13;
verum end;
hence
m,n -cut c is directed Chain of G
by GRAPH_1:def 13; verum