theorem Th47: :: SPRECT_2:47

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,i,j)) misses L~ (mid (f,m,n))