let a, b be Real; :: thesis: ( a < b implies (a + b) / 2 < b )
assume a < b ; :: thesis: (a + b) / 2 < b
then a + b < b + b by XREAL_1:8;
then (a + b) / 2 < (2 * b) / 2 by XREAL_1:74;
hence (a + b) / 2 < b ; :: thesis: verum