let f be real-valued Function; :: thesis: for r1, r2 being Real st f <= r1 & r1 <= r2 holds
f <= r2
let r1, r2 be Real; :: thesis: ( f <= r1 & r1 <= r2 implies f <= r2 )
assume that
A1: f <= r1 and
A2: r1 <= r2 ; :: thesis: f <= r2
let x be object ; :: according to NUMBER08:def 4 :: thesis: ( x in dom f implies f . x <= r2 )
assume x in dom f ; :: thesis: f . x <= r2
then f . x <= r1 by A1;
hence f . x <= r2 by A2, XXREAL_0:2; :: thesis: verum