let i, j, m, n be Element of NAT ; :: thesis: for f being non 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))
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) implies L~ (mid (f,j,i)) misses L~ (mid (f,m,n)) )
mid (f,i,j) = Rev (mid (f,j,i)) by JORDAN4:18;
then L~ (mid (f,i,j)) = L~ (mid (f,j,i)) by SPPOL_2:22;
hence ( 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) implies L~ (mid (f,j,i)) misses L~ (mid (f,m,n)) ) by Th51; :: thesis: verum