theorem Th11: :: MSSCYC_1:12

for m, n being Nat
for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds
not (m,n) -cut f is empty