theorem
:: INTEGR14:24
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
)
)