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

(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