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 A1: ( 1 <= m & m <= n & n <= len p ) ; :: thesis: m,n -cut p is Path of G

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

end;

end;