theorem :: INTEGRA8:50

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral ((- sin),A) = 0