PI / 4 < PI / 1 by XREAL_1:76;
hence arccos ((sqrt 2) / 2) = PI / 4 by Th13, SIN_COS6:92; :: thesis: verum