let f be constant standard special_circular_sequence; :: thesis: for i, j being 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 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 Th37;
then ( Rev (Rev (mid (f,i,j))) = mid (f,i,j) & Rev (mid (f,i,j)) is S-Sequence_in_R2 ) by FINSEQ_6:196;
hence mid (f,i,j) is S-Sequence_in_R2 ; :: thesis: verum