PI in ].0,4.[ by SIN_COS:def 28;
then A1: 0 < PI by XXREAL_1:4;
then PI / 4 < PI / 2 by XREAL_1:76;
then (PI / 4) * (- 1) > (PI / 2) * (- 1) by XREAL_1:69;
hence arcsin (- ((sqrt 2) / 2)) = - (PI / 4) by A1, Th8, SIN_COS6:69; :: thesis: verum