let t, r, s be real number ; :: thesis: ( t in ].r,s.[ implies abs t < max ((abs r),(abs s)) )
assume A1: t in ].r,s.[ ; :: thesis: abs t < max ((abs r),(abs s))
reconsider r = r, t = t, s = s as Real by XREAL_0:def 1;
A2: r < t by A1, XXREAL_1:4;
A3: t < s by A1, XXREAL_1:4;

per cases ( t >= 0 or t < 0 ) ;

suppose A4: t >= 0 ; :: thesis: abs t < max ((abs r),(abs s))

then t = abs t by ABSVALUE:def 1;
then abs t < abs s by A3, A4, ABSVALUE:def 1;
hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; :: thesis: verum

end;

suppose A5: t < 0 ; :: thesis: abs t < max ((abs r),(abs s))

then A6: - t = abs t by ABSVALUE:def 1;
- r = abs r by A2, A5, ABSVALUE:def 1;
then abs t < abs r by A2, A6, XREAL_1:24;
hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; :: thesis: verum

end;

end;