let r, s be real number ; :: thesis: for a, b being real number st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]
let a, b be real number ; :: thesis: ( r in [.a,b.] & s in [.a,b.] implies (r + s) / 2 in [.a,b.] )
assume that
A1: r in [.a,b.] and
A2: s in [.a,b.] ; :: thesis: (r + s) / 2 in [.a,b.]
reconsider a = a, b = b, r = r, s = s as Real by XREAL_0:def 1;
( a <= r & a <= s ) by A1, A2, XXREAL_1:1;
then a + a <= r + s by XREAL_1:9;
then A3: (a + a) / 2 <= (r + s) / 2 by XREAL_1:74;
( r <= b & s <= b ) by A1, A2, XXREAL_1:1;
then r + s <= b + b by XREAL_1:9;
then (r + s) / 2 <= (b + b) / 2 by XREAL_1:74;
hence (r + s) / 2 in [.a,b.] by A3; :: thesis: verum