let f be constant standard special_circular_sequence; :: thesis: for i, j being Nat st i > j & ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) holds
mid (f,i,j) is S-Sequence_in_R2
let i, j be Nat; :: thesis: ( i > j & ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) implies mid (f,i,j) is S-Sequence_in_R2 )
assume that
A1: i > j and
A2: ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) ; :: thesis: mid (f,i,j) is S-Sequence_in_R2
A3: Rev (mid (f,j,i)) = mid (f,i,j) by FINSEQ_6:196;

per cases ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) by A2;

suppose ( 1 < j & i <= len f ) ; :: thesis: mid (f,i,j) is S-Sequence_in_R2

then mid (f,j,i) is S-Sequence_in_R2 by A1, JORDAN4:40;
hence mid (f,i,j) is S-Sequence_in_R2 by A3; :: thesis: verum

end;

suppose A4: ( 1 <= j & i < len f ) ; :: thesis: mid (f,i,j) is S-Sequence_in_R2

then i + 1 <= len f by NAT_1:13;
then mid (f,j,i) is S-Sequence_in_R2 by A1, A4, JORDAN4:39;
hence mid (f,i,j) is S-Sequence_in_R2 by A3; :: thesis: verum

end;

end;