let T1, T2 be _Theta; :: thesis: for epsilon1, epsilon2 being Real st T1 * epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1 holds
ex T being _Theta st epsilon2 = T * epsilon1
let epsilon1, epsilon2 be Real; :: thesis: ( T1 * epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1 implies ex T being _Theta st epsilon2 = T * epsilon1 )
assume A1: ( T1 * epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1 ) ; :: thesis: ex T being _Theta st epsilon2 = T * epsilon1

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

suppose A2: epsilon1 = 0 ; :: thesis: ex T being _Theta st epsilon2 = T * epsilon1

then ( epsilon2 = 0 & 0 = 0 * 0 ) by A1;
hence ex T being _Theta st epsilon2 = T * epsilon1 by A2; :: thesis: verum

end;

suppose A3: epsilon1 > 0 ; :: thesis: ex T being _Theta st epsilon2 = T * epsilon1

then ( - 1 <= T1 & T1 <= epsilon2 / epsilon1 & epsilon2 / epsilon1 <= T2 & T2 <= 1 ) by A1, XREAL_1:77, XREAL_1:79, Def1;
then ( - 1 <= epsilon2 / epsilon1 & epsilon2 / epsilon1 <= 1 ) by XXREAL_0:2;
then reconsider T = epsilon2 / epsilon1 as _Theta by Def1;
T * epsilon1 = epsilon2 by A3, XCMPLX_1:87;
hence ex T being _Theta st epsilon2 = T * epsilon1 ; :: thesis: verum

end;

suppose A4: epsilon1 < 0 ; :: thesis: ex T being _Theta st epsilon2 = T * epsilon1

( 1 >= T1 & T1 >= epsilon2 / epsilon1 & epsilon2 / epsilon1 >= T2 & T2 >= - 1 ) by A1, A4, XREAL_1:78, XREAL_1:80, Def1;
then ( - 1 <= epsilon2 / epsilon1 & epsilon2 / epsilon1 <= 1 ) by XXREAL_0:2;
then reconsider T = epsilon2 / epsilon1 as _Theta by Def1;
T * epsilon1 = epsilon2 by A4, XCMPLX_1:87;
hence ex T being _Theta st epsilon2 = T * epsilon1 ; :: thesis: verum

end;

end;