PI in ].0,4.[ by SIN_COS:def 32;
then A1: 0 < PI by XXREAL_1:4;
then PI / 4 < PI / 2 by XREAL_1:78;
hence arcsin ((sqrt 2) / 2) = PI / 4 by A1, Th7, SIN_COS6:70; :: thesis: verum