now

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

now

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

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

then A18: PI / 2 < r2 by A3, XXREAL_0:2;

now

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

suppose A19: r2 < (3 / 2) * PI ; :: thesis: sin . r2 < sin . r1

then r1 < (3 / 2) * PI by A3, XXREAL_0:2;
then r1 in ].(PI / 2),((3 / 2) * PI ).[ by A17, XXREAL_1:4;
then A20: r1 in ].(PI / 2),((3 / 2) * PI ).[ /\ (dom sin ) by A4, XBOOLE_0:def 4;
r2 in ].(PI / 2),((3 / 2) * PI ).[ by A18, A19, XXREAL_1:4;
then r2 in ].(PI / 2),((3 / 2) * PI ).[ /\ (dom sin ) by A11, XBOOLE_0:def 4;
hence sin . r2 < sin . r1 by A3, A20, Th36, RFUNCT_2:44; :: thesis: verum

end;

suppose A21: r2 = (3 / 2) * PI ; :: thesis: not sin . r2 >= sin . r1

then r1 in ].(PI / 2),((3 / 2) * PI ).[ by A3, A17, XXREAL_1:4;
then r1 in ].(PI / 2),((3 / 2) * PI ).[ /\ (dom sin ) by A4, XBOOLE_0:def 4;
then A22: sin . ((r1 + r2) / 2) < sin . r1 by A12, A15, Th36, RFUNCT_2:44;
assume sin . r2 >= sin . r1 ; :: thesis: contradiction
hence contradiction by A6, A16, A21, A22, SIN_COS:81, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

suppose r2 < (3 / 2) * PI ; :: thesis: not sin . r2 >= sin . r1

then r2 in ].(PI / 2),((3 / 2) * PI ).[ by A3, A23, XXREAL_1:4;
then r2 in ].(PI / 2),((3 / 2) * PI ).[ /\ (dom sin ) by A11, XBOOLE_0:def 4;
then A24: sin . r2 < sin . ((r1 + r2) / 2) by A14, A15, Th36, RFUNCT_2:44;
assume sin . r2 >= sin . r1 ; :: thesis: contradiction
hence contradiction by A10, A5, A23, A24, SIN_COS:81, XXREAL_0:1; :: thesis: verum

end;

suppose r2 = (3 / 2) * PI ; :: thesis: sin . r2 < sin . r1

hence sin . r2 < sin . r1 by A23, 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),((3 / 2) * PI ).] is decreasing by RFUNCT_2:44; :: thesis: verum