PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then ( PI / 4 > 0 & PI / 2 > 0 ) by XREAL_1:141;
then A2: 0 < (PI / 4) + (PI / 2) ;
(3 / 4) * PI < 1 * PI by A1, XREAL_1:70;
hence arccos (- ((sqrt 2) / 2)) = (3 * PI ) / 4 by A2, Th14, SIN_COS6:94; :: thesis: verum