A1: sqrt 2 > 0 by SQUARE_1:25;
cos ((PI / 2) / 2) = sqrt ((1 + (cos (PI / 2))) / 2) by Lm3, Th12
.= 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 cos (PI / 4) = (sqrt 2) / 2 by SQUARE_1:def 2; :: thesis: verum