let x be real number ; :: 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:92
.= 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:88
.= sqrt ((2 * ((sec (x / 2)) ^2 )) / (2 * ((tan (x / 2)) ^2 ))) by A3, A4, XCMPLX_1:88
.= sqrt (((sec (x / 2)) ^2 ) / ((tan (x / 2)) ^2 )) by XCMPLX_1:92
.= sqrt (((sec (x / 2)) / (tan (x / 2))) ^2 ) by XCMPLX_1:77
.= sqrt ((cosec (x / 2)) ^2 ) by A2, Th1
.= abs (cosec (x / 2)) by COMPLEX1:158 ;

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;