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

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

then ( 1 <= m & m <= len p & 1 <= n & n <= len p ) by XXREAL_0:2;
then ( m in dom p & n in dom p ) by FINSEQ_3:25;
then smid (p,m,n) = (m,n) -cut p by FINSEQ_8:29;
hence (m,n) -cut p is _trivial ; :: thesis: verum

end;

suppose ( not 1 <= m or not m <= n or not n <= len p ) ; :: thesis: (m,n) -cut p is _trivial

hence (m,n) -cut p is _trivial by FINSEQ_6:def 4; :: thesis: verum

end;

end;