let th be real number ; :: thesis:
assume A1: ( th in ].0 ,(PI / 2).[ & cos . th <= 0 ) ; :: thesis:
cos | REAL is continuous by Th72, FDIFF_1:33;
then A2: cos | [.0 ,th.] is continuous by FCONT_1:17;
A3: 0 < th by A1, XXREAL_1:4;
A4: th is Real by XREAL_0:def 1;
A5: [.(cos . 0 ),(cos . th).] \/ [.(cos . th),(cos . 0 ).] = [.(cos . th),(cos . 0 ).] by A1, Th33, XXREAL_1:222;
0 in [.(cos . th),(cos . 0 ).] by A1, Th33, XXREAL_1:1;
then ex th2 being Real st
( th2 in [.0 ,th.] & cos . th2 = 0 ) by A2, A3, A4, A5, Th27, FCONT_2:16;
then consider th2 being Real such that
A6: ( th2 in [.0 ,th.] & 0 < th & cos . th2 = 0 ) by A3;
A7: ( 0 <= th2 & th2 <= th & th < PI / 2 ) by A1, A6, XXREAL_1:1, XXREAL_1:4;
then ( 0 < th2 & th2 < PI / 2 ) by A6, Th33, XXREAL_0:2;
then A8: ( 0 / 2 < th2 / 2 & th2 / 2 < (PI / 2) / 2 ) by XREAL_1:76;
PI in ].0 ,4.[ by Def32;
then ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then PI / 4 < 4 / 4 by XREAL_1:76;
then A9: ( 0 < th2 / 2 & th2 / 2 < 1 ) by A8, XXREAL_0:2;
0 = cos . ((th2 / 2) + (th2 / 2)) by A6
.= ((cos . (th2 / 2)) ^2 ) - ((sin . (th2 / 2)) * (sin . (th2 / 2))) by Th79
.= ((cos . (th2 / 2)) - (sin . (th2 / 2))) * ((cos . (th2 / 2)) + (sin . (th2 / 2))) ;
then B10: ( (cos . (th2 / 2)) - (sin . (th2 / 2)) = 0 or (cos . (th2 / 2)) + (sin . (th2 / 2)) = 0 ) ;
A11: th2 / 2 in ].0 ,1.[ by A9, XXREAL_1:4;
A12: ].0 ,1.[ c= [.0 ,1.] by XXREAL_1:25;
then A13: cos . (th2 / 2) > 0 by A11, Th74;
A14: sin . (th2 / 2) >= - 0 by A11, A12, Lm22;
( 2 * th2 in ].0 ,4.[ & tan . ((2 * th2) / 4) = 1 )

proof

( 4 * 0 < 4 * (th2 / 2) & 4 * (th2 / 2) < 4 * 1 ) by A9, XREAL_1:70;
hence 2 * th2 in ].0 ,4.[ by XXREAL_1:4; :: thesis:
(sin . (th2 / 2)) * ((cos . (th2 / 2)) " ) = 1 by B10, A13, A14, XCMPLX_0:def 7;
hence tan . ((2 * th2) / 4) = 1 by A11, Th75, RFUNCT_1:def 4; :: thesis:

end;

then 2 * th2 = PI by Def32;
hence contradiction by A7; :: thesis: