let x be Real; :: thesis: ( sin (x / 2) <> 0 & cos (x / 2) <> 0 & 1 - ((tan (x / 2)) ^2) <> 0 & not cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) implies cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
assume that
A1: sin (x / 2) <> 0 and
A2: cos (x / 2) <> 0 and
A3: 1 - ((tan (x / 2)) ^2) <> 0 ; :: thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2);
A4: ((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)) = (1 + ((tan (x / 2)) ^2)) - (1 - ((tan (x / 2)) ^2)) by A2, Th11
.= 2 * ((tan (x / 2)) ^2) ;
sqrt ((2 * (sec x)) / ((sec x) - 1)) = sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) - 1)) by A1, A2, Th13
.= sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1)) by A1, A2, Th13 ;
then A5: sqrt ((2 * (sec x)) / ((sec x) - 1)) = sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:91
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2)))))
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:87
.= sqrt ((2 * ((sec (x / 2)) ^2)) / (2 * ((tan (x / 2)) ^2))) by A3, A4, XCMPLX_1:87
.= sqrt (((sec (x / 2)) ^2) / ((tan (x / 2)) ^2)) by XCMPLX_1:91
.= sqrt (((sec (x / 2)) / (tan (x / 2))) ^2) by XCMPLX_1:76
.= sqrt ((cosec (x / 2)) ^2) by A2, Th1
.= |.(cosec (x / 2)).| by COMPLEX1:72 ;

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

suppose cosec (x / 2) >= 0 ; :: thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )

hence ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) ) by A5, ABSVALUE:def 1; :: thesis: verum

end;

suppose cosec (x / 2) < 0 ; :: thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )

then (sqrt ((2 * (sec x)) / ((sec x) - 1))) * (- 1) = (- (cosec (x / 2))) * (- 1) by A5, ABSVALUE:def 1;
hence ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) ) ; :: thesis: verum

end;

end;