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