PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then PI / 4 < PI / 2 by XREAL_1:78;
then A2: (PI / 4) * (- 1) > (PI / 2) * (- 1) by XREAL_1:71;
0 / 4 < PI / 4 by A1, XREAL_1:76;
then A3: 0 * (- 1) > (PI / 4) * (- 1) by XREAL_1:71;
0 / 2 < PI / 2 by A1, XREAL_1:76;
hence arcsin (- ((sqrt 2) / 2)) = - (PI / 4) by A2, A3, Th8, SIN_COS6:70; :: thesis: verum