A1: sqrt 2 > 0 by SQUARE_1:93;
A2: cos (- (PI / 2)) = sin ((PI / 2) - (- (PI / 2))) by SIN_COS:84
.= 0 by SIN_COS:82 ;
sin ((- (PI / 2)) / 2) = - (sqrt ((1 - (cos (- (PI / 2)))) / 2)) by Lm2, Th6;
then sin (- (PI / 4)) = - (1 / (sqrt 2)) by A2, SQUARE_1:83, SQUARE_1:99
.= - (((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2))) by A1, XCMPLX_1:92
.= - (((sqrt 2) * 1) / ((sqrt 2) ^2 )) ;
hence sin (- (PI / 4)) = - ((sqrt 2) / 2) by SQUARE_1:def 4; :: thesis: verum