theorem Diesel3: :: MOEBIUS3:21

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) < 1 / n