theorem Th49: :: SPRECT_2:49

for i, j, m, n being Nat
for f being constant standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds
L~ (mid (f,j,i)) misses L~ (mid (f,n,m))