A1: sqrt 2 > 0 by SQUARE_1:25;
sin ((PI / 2) / 2) = sqrt ((1 - (cos (PI / 2))) / 2) by Lm1, Th5;
then sin (PI / 4) = 1 / (sqrt 2) by SIN_COS:77, SQUARE_1:18, SQUARE_1:30
.= ((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) by A1, XCMPLX_1:91
.= ((sqrt 2) * 1) / ((sqrt 2) ^2) ;
hence sin (PI / 4) = (sqrt 2) / 2 by SQUARE_1:def 2; :: thesis: verum