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;

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;