now :: thesis: for r1, r2 being Real st r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r1 < r2 holds
sin . r2 > sin . r1

let r1, r2 be Real; :: thesis: ( r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r1 < r2 implies sin . r2 > sin . r1 )
assume that
A1: r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) and
A2: r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) and
A3: r1 < r2 ; :: thesis: sin . r2 > sin . r1
A4: r1 in dom sin by A1, XBOOLE_0:def 4;
set r3 = (r1 + r2) / 2;
r1 in [.(- (PI / 2)),(PI / 2).] by A1, XBOOLE_0:def 4;
then A5: - (PI / 2) <= r1 by XXREAL_1:1;
|.(sin ((r1 + r2) / 2)).| <= 1 by SIN_COS:27;
then A6: |.(sin . ((r1 + r2) / 2)).| <= 1 by SIN_COS:def 17;
then A7: sin . ((r1 + r2) / 2) <= 1 by ABSVALUE:5;
r2 in [.(- (PI / 2)),(PI / 2).] by A2, XBOOLE_0:def 4;
then A8: r2 <= PI / 2 by XXREAL_1:1;
A9: r1 < (r1 + r2) / 2 by A3, XREAL_1:226;
then A10: - (PI / 2) < (r1 + r2) / 2 by A5, XXREAL_0:2;
A11: (r1 + r2) / 2 < r2 by A3, XREAL_1:226;
then (r1 + r2) / 2 < PI / 2 by A8, XXREAL_0:2;
then (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ by A10, XXREAL_1:4;
then A12: (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by SIN_COS:24, XBOOLE_0:def 4;
|.(sin r2).| <= 1 by SIN_COS:27;
then |.(sin . r2).| <= 1 by SIN_COS:def 17;
then A13: sin . r2 >= - 1 by ABSVALUE:5;
A14: r2 in dom sin by A2, XBOOLE_0:def 4;
A15: sin . ((r1 + r2) / 2) >= - 1 by A6, ABSVALUE:5;

now :: thesis: sin . r2 > sin . r1

per cases ( - (PI / 2) < r1 or - (PI / 2) = r1 ) by A5, XXREAL_0:1;

suppose A16: - (PI / 2) < r1 ; :: thesis: sin . r2 > sin . r1

then A17: - (PI / 2) < r2 by A3, XXREAL_0:2;

now :: thesis: sin . r2 > sin . r1

per cases ( r2 < PI / 2 or r2 = PI / 2 ) by A8, XXREAL_0:1;

suppose A18: r2 < PI / 2 ; :: thesis: sin . r2 > sin . r1

then r1 < PI / 2 by A3, XXREAL_0:2;
then r1 in ].(- (PI / 2)),(PI / 2).[ by A16, XXREAL_1:4;
then A19: r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by A4, XBOOLE_0:def 4;
r2 in ].(- (PI / 2)),(PI / 2).[ by A17, A18, XXREAL_1:4;
then r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by A14, XBOOLE_0:def 4;
hence sin . r2 > sin . r1 by A3, A19, Th19, RFUNCT_2:20; :: thesis: verum

end;

suppose A20: r2 = PI / 2 ; :: thesis: not sin . r2 <= sin . r1

then r1 in ].(- (PI / 2)),(PI / 2).[ by A3, A16, XXREAL_1:4;
then r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by A4, XBOOLE_0:def 4;
then A21: sin . ((r1 + r2) / 2) > sin . r1 by A9, A12, Th19, RFUNCT_2:20;
assume sin . r2 <= sin . r1 ; :: thesis: contradiction
hence contradiction by A7, A20, A21, SIN_COS:76, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence sin . r2 > sin . r1 ; :: thesis: verum

end;

suppose A22: - (PI / 2) = r1 ; :: thesis: sin . r2 > sin . r1

now :: thesis: not sin . r2 <= sin . r1

per cases ( r2 < PI / 2 or r2 = PI / 2 ) by A8, XXREAL_0:1;

suppose r2 < PI / 2 ; :: thesis: not sin . r2 <= sin . r1

then r2 in ].(- (PI / 2)),(PI / 2).[ by A3, A22, XXREAL_1:4;
then r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by A14, XBOOLE_0:def 4;
then A23: sin . r2 > sin . ((r1 + r2) / 2) by A11, A12, Th19, RFUNCT_2:20;
assume sin . r2 <= sin . r1 ; :: thesis: contradiction
then sin . r2 <= - 1 by A22, SIN_COS:30, SIN_COS:76;
hence contradiction by A15, A13, A23, XXREAL_0:1; :: thesis: verum

end;

suppose r2 = PI / 2 ; :: thesis: sin . r2 > sin . r1

hence sin . r2 > sin . r1 by A22, SIN_COS:30, SIN_COS:76; :: thesis: verum

end;

end;

end;

hence sin . r2 > sin . r1 ; :: thesis: verum

end;

end;

end;

hence sin . r2 > sin . r1 ; :: thesis: verum

end;

hence sin | [.(- (PI / 2)),(PI / 2).] is increasing by RFUNCT_2:20; :: thesis: verum