let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st i < j & ( ( 1 < i & j <= len f ) or ( 1 <= i & j < len f ) ) holds
mid f,i,j is S-Sequence_in_R2
let i, j be Element of NAT ; :: thesis: ( i < j & ( ( 1 < i & j <= len f ) or ( 1 <= i & j < len f ) ) implies mid f,i,j is S-Sequence_in_R2 )
assume ( i < j & ( ( 1 < i & j <= len f ) or ( 1 <= i & j < len f ) ) ) ; :: thesis: mid f,i,j is S-Sequence_in_R2
then mid f,j,i is S-Sequence_in_R2 by Th41;
then ( Rev (Rev (mid f,i,j)) = mid f,i,j & Rev (mid f,i,j) is S-Sequence_in_R2 ) by FINSEQ_6:29, JORDAN4:30;
hence mid f,i,j is S-Sequence_in_R2 by SPPOL_2:47; :: thesis: verum