let s, r, t be real number ; :: thesis: ( ( s - r < t & s + r > t ) iff abs (t - s) < r )
thus ( s - r < t & s + r > t implies abs (t - s) < r ) :: thesis: ( abs (t - s) < r implies ( s - r < t & s + r > t ) )

proof

assume A1: ( s - r < t & s + r > t ) ; :: thesis: abs (t - s) < r
then (- r) + s < t ;
then A2: - r < t - s by XREAL_1:22;
t - s < r by A1, XREAL_1:21;
hence abs (t - s) < r by A2, SEQ_2:9; :: thesis: verum

end;

assume A3: abs (t - s) < r ; :: thesis: ( s - r < t & s + r > t )
then - r < t - s by SEQ_2:9;
then A4: s + (- r) < t by XREAL_1:22;
t - s < r by A3, SEQ_2:9;
hence ( s - r < t & s + r > t ) by A4, XREAL_1:21; :: thesis: verum