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,i,j) misses L~ (mid f,n,m)
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,i,j) misses L~ (mid f,n,m) )
mid f,n,m = Rev (mid f,m,n) by JORDAN4:30;
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 Th51; :: thesis: verum