theorem :: INTEGR11:15

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