theorem :: INTEGRA8:79

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