let T be _Theta; :: thesis: for lambda, epsilon1, epsilon2 being Real st lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1 holds
ex T1 being _Theta st lambda = T1 * epsilon2
let lambda, epsilon1, epsilon2 be Real; :: thesis: ( lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1 implies ex T1 being _Theta st lambda = T1 * epsilon2 )
assume A1: ( lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1 ) ; :: thesis: ex T1 being _Theta st lambda = T1 * epsilon2
( |.epsilon1.| = epsilon1 & |.epsilon2.| = epsilon2 ) by A1, ABSVALUE:def 1;
hence ex T1 being _Theta st lambda = T1 * epsilon2 by Th2, A1; :: thesis: verum