let G be Graph; :: thesis: for p being Path of G
for n, m being Nat holds (m,n) -cut p is Path of G
let p be Path of G; :: thesis: for n, m being Nat holds (m,n) -cut p is Path of G
let n, m be Nat; :: thesis: (m,n) -cut p is Path of G

per cases ( not 1 <= m or not n <= len p or m > n or ( 1 <= m & m <= n & n <= len p ) ) ;

suppose ( not 1 <= m or not n <= len p or m > n ) ; :: thesis: (m,n) -cut p is Path of G

then (m,n) -cut p = {} by FINSEQ_6:def 4;
hence (m,n) -cut p is Path of G by GRAPH_1:14; :: thesis: verum

end;

suppose ( 1 <= m & m <= n & n <= len p ) ; :: thesis: (m,n) -cut p is Path of G

then reconsider q = (m,n) -cut p as Chain of G by GRAPH_2:41;
assume (m,n) -cut p is not Path of G ; :: thesis: contradiction
then consider a, b being Nat such that
A1: 1 <= a and
A2: a < b and
A3: b <= len q and
A4: q . a = q . b by GRAPH_1:def 16;
1 <= b by A1, A2, XXREAL_0:2;
then b in dom q by A3, FINSEQ_3:25;
then consider kb being Nat such that
A5: ( kb in dom p & p . kb = q . b ) and
A6: kb + 1 = m + b and
m <= kb and
kb <= n by Th2;
a <= len q by A2, A3, XXREAL_0:2;
then a in dom q by A1, FINSEQ_3:25;
then consider ka being Nat such that
A7: ( ka in dom p & p . ka = q . a ) and
A8: ka + 1 = m + a and
m <= ka and
ka <= n by Th2;
ka = kb by A4, A7, A5, FUNCT_1:def 4;
hence contradiction by A2, A8, A6; :: thesis: verum

end;

end;