( PI / 6 < PI / 2 & PI / 3 < PI / 2 & - (PI / 2) <= PI / 6 & - (PI / 2) <= PI / 3 ) by XREAL_1:76, COMPTRIG:5;
hence ( arcsin (1 / 2) = PI / 6 & arcsin ((sqrt 3) / 2) = PI / 3 ) by Thm9, Thm11, SIN_COS6:69; :: thesis: verum