for n being Nat
for r being Real
for A being non empty closed_interval Subset of REAL st A = [.0,r.] & r >= 0 holds
|.(integral (((#Z (2 * n)) / ((#Z 0) + (#Z 2))),A)).| <= (1 / ((2 * n) + 1)) * (r |^ ((2 * n) + 1))