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