PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then A2: PI / 4 < PI / 1 by XREAL_1:78;
0 / 4 < PI / 4 by A1, XREAL_1:76;
hence arccos ((sqrt 2) / 2) = PI / 4 by A2, Th13, SIN_COS6:94; :: thesis: verum