theorem
:: INTEGR14:25
for
A
being non
empty
closed_interval
Subset
of
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
cosec
)
&
Z
=
dom
cot
&
cot

A
is
continuous
holds
integral
(
cot
,
A
)
=
(
(

(
ln
*
cosec
)
)
.
(
upper_bound
A
)
)

(
(

(
ln
*
cosec
)
)
.
(
lower_bound
A
)
)