let g, r be real number ; :: thesis: ( ( - g < r & r < g ) iff abs r < g )
thus ( - g < r & r < g implies abs r < g ) :: thesis: ( abs r < g implies ( - g < r & r < g ) )

proof

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

now

assume A4: abs r = g ; :: thesis: contradiction

now

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 abs r < g by A3, XXREAL_0:1; :: thesis: verum

end;

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

now

assume r = - g ; :: thesis: contradiction
then abs 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