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

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

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

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

end;

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

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

end;

end;