let r be Real; :: thesis: ( r > 0 implies ex s being Real st
( 0 <= s & s < PI / 2 & tan . s = r ) )
assume A1: r > 0 ; :: thesis: ex s being Real st
( 0 <= s & s < PI / 2 & tan . s = r )
set e = 1 / (2 * r);
set P = PI / 2;
A2: PI / 2 in REAL by XREAL_0:def 1;
dom sin = REAL by FUNCT_2:def 1;
then consider s1 being Real such that
A3: ( 0 < s1 & ( for x1 being Real st x1 in dom sin & |.(x1 - (PI / 2)).| < s1 holds
|.((sin . x1) - (sin . (PI / 2))).| < 1 / 2 ) ) by A2, FCONT_1:def 2, FCONT_1:3;
A4: ( dom cos = REAL & dom sin = REAL ) by FUNCT_2:def 1;
then consider s2 being Real such that
A5: ( 0 < s2 & ( for x1 being Real st x1 in dom cos & |.(x1 - (PI / 2)).| < s2 holds
|.((cos . x1) - (cos . (PI / 2))).| < 1 / (2 * r) ) ) by A1, FCONT_1:3, A2, FCONT_1:def 2;
set m = min (s1,s2);
set M = min ((min (s1,s2)),(PI / 2));
set m2 = (min ((min (s1,s2)),(PI / 2))) / 2;
( 0 < min (s1,s2) & 0 < PI / 2 ) by A3, A5, XXREAL_0:21;
then A6: min ((min (s1,s2)),(PI / 2)) > 0 by XXREAL_0:21;
then A7: ( (min ((min (s1,s2)),(PI / 2))) / 2 > 0 & (min ((min (s1,s2)),(PI / 2))) / 2 < min ((min (s1,s2)),(PI / 2)) ) by XREAL_1:216;
set X = (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2);
A8: (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in REAL by XREAL_0:def 1;
A9: (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) < PI / 2 by A6, XREAL_1:37;
A10: |.(((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) - (PI / 2)).| = - (((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) - (PI / 2)) by A6, ABSVALUE:def 1;
A11: ( min ((min (s1,s2)),(PI / 2)) <= min (s1,s2) & min ((min (s1,s2)),(PI / 2)) <= PI / 2 & min (s1,s2) <= s1 & min (s1,s2) <= s2 ) by XXREAL_0:17;
then ( min ((min (s1,s2)),(PI / 2)) <= s1 & min ((min (s1,s2)),(PI / 2)) <= s2 ) by XXREAL_0:2;
then A12: ( (min ((min (s1,s2)),(PI / 2))) / 2 < s1 & (min ((min (s1,s2)),(PI / 2))) / 2 < s2 & (min ((min (s1,s2)),(PI / 2))) / 2 < PI / 2 ) by A11, A7, XXREAL_0:2;
then A13: |.((cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) - (cos . (PI / 2))).| < 1 / (2 * r) by A10, A4, A5, XREAL_0:def 1;
A14: (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) > 0 by A12, XREAL_1:50;
then (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in ].0,(PI / 2).[ by A9, XXREAL_1:4;
then A15: ( cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) > 0 & cos . (PI / 2) = 0 ) by SIN_COS:80, SIN_COS:77;
cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) < 1 / (2 * r) by A15, A13, ABSVALUE:def 1;
then A16: ( 1 / (cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) > 1 / (1 / (2 * r)) & 1 / (1 / (2 * r)) = 2 * r ) by XREAL_1:76, A15;
( sin ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) < 1 & sin . (PI / 2) = 1 & sin ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) = sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) ) by SIN_COS6:30, A9, A14, SIN_COS:77;
then |.((sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) - 1).| = - ((sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) - 1) by ABSVALUE:def 1, XREAL_1:49;
then 1 - (sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) < 1 / 2 by SIN_COS:77, A10, A3, A4, XREAL_0:def 1, A12;
then sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) > 1 - (1 / 2) by XREAL_1:11;
then A17: (sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) / (cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) > (1 / 2) / (cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) by A15, XREAL_1:74;
(1 / 2) / (cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) > (1 / 2) * (2 * r) by A16, XREAL_1:68;
then A18: (sin . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) / (cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))) > r by A17, XXREAL_0:2;
not cos . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) in {0} by A15, TARSKI:def 1;
then not (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in cos " {0} by FUNCT_1:def 7;
then (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in (dom cos) \ (cos " {0}) by A8, A4, XBOOLE_0:def 5;
then (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in (dom sin) /\ ((dom cos) \ (cos " {0})) by A4, XBOOLE_0:def 4;
then (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) in dom tan by RFUNCT_1:def 1;
then A19: tan . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)) > r by A18, RFUNCT_1:def 1;
A20: [.0,((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)).] c= ].(- (PI / 2)),(PI / 2).[ by A9, XXREAL_1:47;
A21: tan | [.0,((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)).] is continuous by A9, XXREAL_1:47, SIN_COS9:5, FCONT_1:16;
A22: [.0,((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)).] c= dom tan by A20, SIN_COS9:1;
r in [.(tan . 0),(tan . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))).] by A1, A19, XXREAL_1:1, SIN_COS9:41;
then r in [.(tan . 0),(tan . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))).] \/ [.(tan . ((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2))),(tan . 0).] by XBOOLE_0:def 3;
then consider s being Real such that
A23: ( s in [.0,((PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2)).] & r = tan . s ) by A21, A22, A14, FCONT_2:15;
A24: ( 0 <= s & s <= (PI / 2) - ((min ((min (s1,s2)),(PI / 2))) / 2) ) by A23, XXREAL_1:1;
then s < PI / 2 by A6, XREAL_1:37;
hence ex s being Real st
( 0 <= s & s < PI / 2 & tan . s = r ) by A23, A24; :: thesis: verum