PI / 4 < PI / 2 by XREAL_1:76;
hence arcsin ((sqrt 2) / 2) = PI / 4 by Th7, SIN_COS6:69; :: thesis: verum