let i, j, m, n be Nat; :: thesis: 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,n,m))
let f be 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,i,j)) misses L~ (mid (f,n,m)) )
mid (f,n,m) = Rev (mid (f,m,n)) by FINSEQ_6:196;
then L~ (mid (f,n,m)) = L~ (mid (f,m,n)) 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,i,j)) misses L~ (mid (f,n,m)) ) by Th47; :: thesis: verum