let T1 be _Theta; :: thesis: for epsilon being Real st 0 <= epsilon & epsilon <= 1 / 2 holds
ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon)
let epsilon be Real; :: thesis: ( 0 <= epsilon & epsilon <= 1 / 2 implies ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon) )
assume A1: ( 0 <= epsilon & epsilon <= 1 / 2 ) ; :: thesis: ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon)
A2: 1 - epsilon >= 1 - (1 / 2) by A1, XREAL_1:10;
( - 1 <= T1 & T1 <= 1 ) by Def1;
then (- 1) * epsilon <= T1 * epsilon by A1, XREAL_1:64;
then A3: 1 + ((- 1) * epsilon) <= 1 + (T1 * epsilon) by XREAL_1:6;
then 1 / (1 + (T1 * epsilon)) <= 1 / (1 - epsilon) by A2, XREAL_1:118;
then (1 / (1 + (T1 * epsilon))) * epsilon <= (1 / (1 - epsilon)) * epsilon by A1, XREAL_1:64;
then (1 / (1 + (T1 * epsilon))) * epsilon <= (1 * epsilon) / (1 - epsilon) by XCMPLX_1:74;
then A4: (1 * epsilon) / (1 + (T1 * epsilon)) <= (1 * epsilon) / (1 - epsilon) by XCMPLX_1:74;
reconsider I = 1 as _Theta by Def1;
A5: |.(2 * epsilon).| = 2 * epsilon by A1, ABSVALUE:def 1;
A6: ( epsilon / (1 - epsilon) <= epsilon / (1 / 2) & epsilon / (1 / 2) = 2 * epsilon ) by A1, XREAL_1:118, A2;

per cases ( T1 < 0 or T1 >= 0 ) ;

suppose T1 < 0 ; :: thesis: ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon)

then A7: |.((- T1) * (epsilon / (1 + (T1 * epsilon)))).| = (- T1) * (epsilon / (1 + (T1 * epsilon))) by A1, A2, A3, ABSVALUE:def 1;
- T1 <= 1 by Def1;
then (- T1) * (epsilon / (1 + (T1 * epsilon))) <= 1 * (epsilon / (1 + (T1 * epsilon))) by A1, A2, A3, XREAL_1:64;
then (- T1) * (epsilon / (1 + (T1 * epsilon))) <= epsilon / (1 - epsilon) by A4, XXREAL_0:2;
then I * ((- T1) * (epsilon / (1 + (T1 * epsilon)))) <= 2 * epsilon by A6, XXREAL_0:2;
then consider T being _Theta such that
A8: (- T1) * (epsilon / (1 + (T1 * epsilon))) = T * (2 * epsilon) by Th2, A7, A5;
1 - ((T1 * epsilon) / (1 + (T1 * epsilon))) = ((1 + (T1 * epsilon)) / (1 + (T1 * epsilon))) - ((T1 * epsilon) / (1 + (T1 * epsilon))) by A2, A3, XCMPLX_1:60
.= ((1 + (T1 * epsilon)) - (T1 * epsilon)) / (1 + (T1 * epsilon)) by XCMPLX_1:120
.= 1 / (1 + (T1 * epsilon)) ;
then 1 / (1 + (T1 * epsilon)) = 1 - (T1 * (epsilon / (1 + (T1 * epsilon)))) by XCMPLX_1:74;
then 1 / (1 + (T1 * epsilon)) = 1 + ((T * 2) * epsilon) by A8;
hence ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon) ; :: thesis: verum

end;

suppose T1 >= 0 ; :: thesis: ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon)

then A9: |.(T1 * (epsilon / (1 + (T1 * epsilon)))).| = T1 * (epsilon / (1 + (T1 * epsilon))) by A1, ABSVALUE:def 1;
T1 <= 1 by Def1;
then T1 * (epsilon / (1 + (T1 * epsilon))) <= 1 * (epsilon / (1 + (T1 * epsilon))) by A1, A2, A3, XREAL_1:64;
then T1 * (epsilon / (1 + (T1 * epsilon))) <= epsilon / (1 - epsilon) by A4, XXREAL_0:2;
then I * (T1 * (epsilon / (1 + (T1 * epsilon)))) <= 2 * epsilon by A6, XXREAL_0:2;
then consider T being _Theta such that
A10: T1 * (epsilon / (1 + (T1 * epsilon))) = T * (2 * epsilon) by Th2, A9, A5;
1 - ((T1 * epsilon) / (1 + (T1 * epsilon))) = ((1 + (T1 * epsilon)) / (1 + (T1 * epsilon))) - ((T1 * epsilon) / (1 + (T1 * epsilon))) by A2, A3, XCMPLX_1:60
.= ((1 + (T1 * epsilon)) - (T1 * epsilon)) / (1 + (T1 * epsilon)) by XCMPLX_1:120
.= 1 / (1 + (T1 * epsilon)) ;
then 1 / (1 + (T1 * epsilon)) = 1 - (T * (2 * epsilon)) by A10, XCMPLX_1:74;
then 1 / (1 + (T1 * epsilon)) = 1 + (((- T) * 2) * epsilon) ;
hence ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon) ; :: thesis: verum

end;

end;