let r, s, t be Real; :: thesis: ( ( s - r < t & s + r > t ) iff |.(t - s).| < r )
thus ( s - r < t & s + r > t implies |.(t - s).| < r ) :: thesis: ( |.(t - s).| < r implies ( s - r < t & s + r > t ) )

proof

assume that
A1: s - r < t and
A2: s + r > t ; :: thesis: |.(t - s).| < r
(- r) + s < t by A1;
then A3: - r < t - s by XREAL_1:20;
t - s < r by A2, XREAL_1:19;
hence |.(t - s).| < r by A3, SEQ_2:1; :: thesis: verum

end;

assume A4: |.(t - s).| < r ; :: thesis: ( s - r < t & s + r > t )
then - r < t - s by SEQ_2:1;
then A5: s + (- r) < t by XREAL_1:20;
t - s < r by A4, SEQ_2:1;
hence ( s - r < t & s + r > t ) by A5, XREAL_1:19; :: thesis: verum