let r, s, t be Real; :: thesis: ( t in ].r,s.[ implies |.t.| < max (|.r.|,|.s.|) )
assume A1: t in ].r,s.[ ; :: thesis: |.t.| < max (|.r.|,|.s.|)
reconsider r = r, t = t, s = s as Real ;
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: |.t.| < max (|.r.|,|.s.|)

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

end;

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

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

end;

end;