(3 / 4) * PI < 1 * PI by XREAL_1:68;
hence arccos (- ((sqrt 2) / 2)) = (3 * PI) / 4 by Th14, SIN_COS6:92; :: thesis: verum