let r, g be Real; :: thesis: ( ( - g < r & r < g ) iff |.r.| < g )
thus ( - g < r & r < g implies |.r.| < g ) :: thesis: ( |.r.| < g implies ( - g < r & r < g ) )

proof

assume that
A1: - g < r and
A2: r < g ; :: thesis: |.r.| < g
A3: |.r.| <= g by A1, A2, ABSVALUE:5;

now :: thesis: not |.r.| = g

assume A4: |.r.| = g ; :: thesis: contradiction

now :: thesis: not r < 0

assume r < 0 ; :: thesis: contradiction
then g = - r by A4, ABSVALUE:def 1;
hence contradiction by A1; :: thesis: verum

end;

hence contradiction by A2, A4, ABSVALUE:def 1; :: thesis: verum

end;

hence |.r.| < g by A3, XXREAL_0:1; :: thesis: verum

end;

assume A5: |.r.| < g ; :: thesis: ( - g < r & r < g )
then A6: - g <= r by ABSVALUE:5;
A7: 0 <= |.r.| by COMPLEX1:46;
A8: 0 < g by A5, COMPLEX1:46;
A9: - g < - 0 by A5, A7;

now :: thesis: not r = - g

assume r = - g ; :: thesis: contradiction
then |.r.| = - (- g) by A9, ABSVALUE:def 1
.= g ;
hence contradiction by A5; :: thesis: verum

end;

hence - g < r by A6, XXREAL_0:1; :: thesis: r < g
thus r < g by A5, A8, ABSVALUE:def 1; :: thesis: verum