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:26;
hence abs t < max (abs r),(abs s) by XXREAL_0:30; :: thesis: verum

end;

end;