let G be Graph; :: thesis: for p being Path of G
for m, n being Element of NAT holds m,n -cut p is Path of G
let p be Path of G; :: thesis: for m, n being Element of NAT holds m,n -cut p is Path of G
let m, n be Element of 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 GRAPH_2:def 1;
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:44;
assume m,n -cut p is not Path of G ; :: thesis: contradiction
then consider a, b being Element of 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 14;
1 <= b by A1, A2, XXREAL_0:2;
then b in dom q by A3, FINSEQ_3:27;
then consider kb being Element of 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:27;
then consider ka being Element of 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 8;
hence contradiction by A2, A8, A6; :: thesis: verum

end;

end;