let i, j, m, n be Nat; 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; ( 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; verum