theorem Th50: :: SPRECT_2:50

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,m,n))