now :: thesis: for r1, r2 being Real st r1 in [.0,PI.] /\ (dom cos) & r2 in [.0,PI.] /\ (dom cos) & r1 < r2 holds
cos . r2 < cos . r1

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

now :: thesis: cos . r2 < cos . r1

per cases ( 0 < r1 or 0 = r1 ) by A12, XXREAL_1:1;

suppose A17: 0 < r1 ; :: thesis: cos . r2 < cos . r1

now :: thesis: cos . r2 < cos . r1

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

suppose A18: r2 < PI ; :: thesis: cos . r2 < cos . r1

then r1 < PI by A3, XXREAL_0:2;
then r1 in ].0,PI.[ by A17, XXREAL_1:4;
then A19: r1 in ].0,PI.[ /\ (dom cos) by A4, XBOOLE_0:def 4;
r2 in ].0,PI.[ by A3, A17, A18, XXREAL_1:4;
then r2 in ].0,PI.[ /\ (dom cos) by A11, XBOOLE_0:def 4;
hence cos . r2 < cos . r1 by A3, A19, Th21, RFUNCT_2:21; :: thesis: verum

end;

suppose A20: r2 = PI ; :: thesis: not cos . r2 >= cos . r1

then r1 in ].0,PI.[ by A3, A17, XXREAL_1:4;
then r1 in ].0,PI.[ /\ (dom cos) by A4, XBOOLE_0:def 4;
then A21: cos . ((r1 + r2) / 2) < cos . r1 by A8, A15, Th21, RFUNCT_2:21;
assume cos . r2 >= cos . r1 ; :: thesis: contradiction
hence contradiction by A6, A16, A20, A21, SIN_COS:76, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

suppose A22: 0 = r1 ; :: thesis: cos . r2 < cos . r1

now :: thesis: not cos . r2 >= cos . r1

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

suppose r2 < PI ; :: thesis: not cos . r2 >= cos . r1

then r2 in ].0,PI.[ by A3, A22, XXREAL_1:4;
then r2 in ].0,PI.[ /\ (dom cos) by A11, XBOOLE_0:def 4;
then A23: cos . r2 < cos . ((r1 + r2) / 2) by A14, A15, Th21, RFUNCT_2:21;
assume cos . r2 >= cos . r1 ; :: thesis: contradiction
hence contradiction by A10, A5, A22, A23, SIN_COS:30, XXREAL_0:1; :: thesis: verum

end;

suppose r2 = PI ; :: thesis: cos . r2 < cos . r1

hence cos . r2 < cos . r1 by A22, SIN_COS:30, SIN_COS:76; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence cos | [.0,PI.] is decreasing by RFUNCT_2:21; :: thesis: verum