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 & t < s ) by A1, XXREAL_1:4;

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

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

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

end;

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

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

end;

end;