theorem :: INTEGRA8:49
for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds
integral ((- sin),A) = - 1