let x be Real; :: 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:91
.= sqrt ((cot (x / 2)) ^2) by XCMPLX_1:76
.= |.(cot (x / 2)).| by COMPLEX1:72 ;

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;