let x be Real; :: thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
A1: sqrt ((1 + (cos x)) / 2) = sqrt ((1 + (cos (2 * (x / 2)))) / 2)
.= sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / 2) by Th7
.= |.(cos (x / 2)).| by COMPLEX1:72 ;

per cases ( cos (x / 2) >= 0 or cos (x / 2) < 0 ) ;

suppose cos (x / 2) >= 0 ; :: thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )

hence ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) ) by A1, ABSVALUE:def 1; :: thesis: verum

end;

suppose cos (x / 2) < 0 ; :: thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )

then (sqrt ((1 + (cos x)) / 2)) * (- 1) = (- (cos (x / 2))) * (- 1) by A1, ABSVALUE:def 1;
hence ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) ) ; :: thesis: verum

end;

end;