let a, b be Real; :: thesis: ( a <= b implies ( a <= (a + b) / 2 & (a + b) / 2 <= b ) )
assume A1: a <= b ; :: thesis: ( a <= (a + b) / 2 & (a + b) / 2 <= b )
2 * a = a + a ;
then 2 * a <= a + b by A1, XREAL_1:7;
then (2 * a) / 2 <= (a + b) / 2 by XREAL_1:72;
hence a <= (a + b) / 2 ; :: thesis: (a + b) / 2 <= b
a + b <= b + b by A1, XREAL_1:7;
then (a + b) / 2 <= (2 * b) / 2 by XREAL_1:72;
hence (a + b) / 2 <= b ; :: thesis: verum