let x be real number ; :: thesis: ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
A1: sqrt ((1 + (cos x)) / (1 - (cos x))) = sqrt ((1 + ((2 * ((cos (x / 2)) ^2 )) - 1)) / (1 - (cos (2 * (x / 2))))) by Th7
.= sqrt ((1 - (1 - (2 * ((cos (x / 2)) ^2 )))) / (1 - (1 - (2 * ((sin (x / 2)) ^2 ))))) by Th7
.= sqrt (((cos (x / 2)) ^2 ) / ((sin (x / 2)) ^2 )) by XCMPLX_1:92
.= sqrt ((cot (x / 2)) ^2 ) by XCMPLX_1:77
.= abs (cot (x / 2)) by COMPLEX1:158 ;

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

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

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

end;

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

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

end;

end;