let r, s be Real; :: thesis: for a, b being Real st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]
let a, b be Real; :: 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 ;
A3: s <= b by A2, XXREAL_1:1;
r <= b by A1, XXREAL_1:1;
then r + s <= b + b by A3, XREAL_1:7;
then A4: (r + s) / 2 <= (b + b) / 2 by XREAL_1:72;
A5: a <= s by A2, XXREAL_1:1;
a <= r by A1, XXREAL_1:1;
then a + a <= r + s by A5, XREAL_1:7;
then (a + a) / 2 <= (r + s) / 2 by XREAL_1:72;
hence (r + s) / 2 in [.a,b.] by A4; :: thesis: verum