let r1, r2 be Real; :: thesis: ( |.r1.| < r2 implies ( - r2 < r1 & r1 < r2 ) )
assume A1: |.r1.| < r2 ; :: thesis: ( - r2 < r1 & r1 < r2 )
then A2: - |.r1.| > - r2 by XREAL_1:24;
( - |.r1.| <= r1 & r1 <= |.r1.| ) by ABSVALUE:4;
hence ( - r2 < r1 & r1 < r2 ) by A1, A2, XXREAL_0:2; :: thesis: verum