let i, j, m, n be Nat; :: thesis: for f being V22() 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))
let f be V22() 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,n,m)) )
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,n,m)) ) by Th48; :: thesis: verum