let x be Real; :: thesis: ( cos (x / 2) >= 0 implies cos (x / 2) = sqrt ((1 + (cos x)) / 2) )
assume A1: cos (x / 2) >= 0 ; :: thesis: cos (x / 2) = sqrt ((1 + (cos x)) / 2)
sqrt ((1 + (cos x)) / 2) = sqrt ((1 + (cos (2 * (x / 2)))) / 2)
.= sqrt ((1 + ((2 * ((cos (x / 2)) ^2 )) - 1)) / 2) by SIN_COS5:7
.= abs (cos (x / 2)) by COMPLEX1:158
.= cos (x / 2) by A1, ABSVALUE:def 1 ;
hence cos (x / 2) = sqrt ((1 + (cos x)) / 2) ; :: thesis: verum