PI in ].0,4.[ by SIN_COS:def 28;
then A1: 0 < PI by XXREAL_1:4;
then (3 / 4) * PI < 1 * PI by XREAL_1:68;
hence arccos (- ((sqrt 2) / 2)) = (3 * PI) / 4 by A1, Th14, SIN_COS6:92; :: thesis: verum