let r, s be Real; :: thesis: ( r < s implies ( r < (r + s) / 2 & (r + s) / 2 < s ) )
assume r < s ; :: thesis: ( r < (r + s) / 2 & (r + s) / 2 < s )
then A1: r / 2 < s / 2 by Lm26;
then (r / 2) + (r / 2) < (r / 2) + (s / 2) by Lm10;
hence r < (r + s) / 2 ; :: thesis: (r + s) / 2 < s
(r / 2) + (s / 2) < (s / 2) + (s / 2) by A1, Lm10;
hence (r + s) / 2 < s ; :: thesis: verum