let x be real number ; :: thesis: ( sin (x / 2) <> 0 & cos (x / 2) <> 0 & 1 - ((tan (x / 2)) ^2 ) <> 0 & not sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) implies sec (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: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2 );
A4: (1 - ((tan (x / 2)) ^2 )) + ((sec (x / 2)) ^2 ) = (1 + ((tan (x / 2)) ^2 )) + (1 - ((tan (x / 2)) ^2 )) by A2, Th11
.= 1 + 1 ;
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) by A3, A4, XCMPLX_1:88
.= abs (sec (x / 2)) by COMPLEX1:158 ;

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

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

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

end;

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

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

end;

end;