let s, r be Real; :: thesis: ( r <= s implies ( r <= (r + s) / 2 & (r + s) / 2 <= s ) )
assume A1: r <= s ; :: thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )

per cases ( r < s or r = s ) by A1, XXREAL_0:1;

suppose r < s ; :: thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )

hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) by XREAL_1:226; :: thesis: verum

end;

suppose r = s ; :: thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s )

hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) ; :: thesis: verum

end;

end;