theorem Th5: :: LEIBNIZ1:5

for A being non empty closed_interval Subset of REAL holds integral (((#Z 0) / ((#Z 0) + (#Z 2))),A) = (arctan . (upper_bound A)) - (arctan . (lower_bound A))