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

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

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

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

end;

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

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

end;

end;