now

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 [.(- (PI / 2)),(PI / 2).] & r1 in dom sin & r2 in [.(- (PI / 2)),(PI / 2).] & r2 in dom sin ) by A1, A2, XBOOLE_0:def 4;
then A5: ( - (PI / 2) <= r1 & r1 <= PI / 2 & - (PI / 2) <= r2 & r2 <= PI / 2 ) by XXREAL_1:1;
set r3 = (r1 + r2) / 2;
abs (sin ((r1 + r2) / 2)) <= 1 by SIN_COS:30;
then abs (sin . ((r1 + r2) / 2)) <= 1 by SIN_COS:def 21;
then A6: ( sin . ((r1 + r2) / 2) >= - 1 & sin . ((r1 + r2) / 2) <= 1 ) by ABSVALUE:12;
abs (sin r2) <= 1 by SIN_COS:30;
then abs (sin . r2) <= 1 by SIN_COS:def 21;
then A7: sin . r2 >= - 1 by ABSVALUE:12;
A8: ( r1 < (r1 + r2) / 2 & (r1 + r2) / 2 < r2 ) by A3, XREAL_1:228;
then ( - (PI / 2) < (r1 + r2) / 2 & (r1 + r2) / 2 < PI / 2 ) by A5, XXREAL_0:2;
then ( (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ & (r1 + r2) / 2 in dom sin ) by SIN_COS:27, XXREAL_1:4;
then A9: (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin ) by XBOOLE_0:def 4;

now

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

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

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

now

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

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

then r1 < PI / 2 by A3, XXREAL_0:2;
then ( r1 in ].(- (PI / 2)),(PI / 2).[ & r2 in ].(- (PI / 2)),(PI / 2).[ ) by A10, A11, A12, XXREAL_1:4;
then ( r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin ) & r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin ) ) by A4, XBOOLE_0:def 4;
hence sin . r2 > sin . r1 by A3, Th35, RFUNCT_2:43; :: thesis: verum

end;

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

then r1 in ].(- (PI / 2)),(PI / 2).[ by A3, A10, XXREAL_1:4;
then r1 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin ) by A4, XBOOLE_0:def 4;
then A14: sin . ((r1 + r2) / 2) > sin . r1 by A8, A9, Th35, RFUNCT_2:43;
assume sin . r2 <= sin . r1 ; :: thesis: contradiction
hence contradiction by A6, A13, A14, SIN_COS:81, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

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

then r2 in ].(- (PI / 2)),(PI / 2).[ by A3, A15, XXREAL_1:4;
then r2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin ) by A4, XBOOLE_0:def 4;
then A16: sin . r2 > sin . ((r1 + r2) / 2) by A8, A9, Th35, RFUNCT_2:43;
assume sin . r2 <= sin . r1 ; :: thesis: contradiction
then sin . r2 <= - 1 by A15, SIN_COS:33, SIN_COS:81;
hence contradiction by A6, A7, A16, XXREAL_0:1; :: thesis: verum

end;

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

hence sin . r2 > sin . r1 by A15, SIN_COS:33, SIN_COS:81; :: 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:43; :: thesis: verum