let
x
be
Real
;
:: thesis:
(
sin
x
<>
0
implies
cos
x
=
(
sin
x
)
*
(
cot
x
)
)
assume
sin
x
<>
0
;
:: thesis:
cos
x
=
(
sin
x
)
*
(
cot
x
)
then
cos
x
=
(
(
sin
x
)
/
(
sin
x
)
)
*
(
cos
x
)
by
XCMPLX_1:88
.=
(
sin
x
)
*
(
cot
x
)
by
XCMPLX_1:75
;
hence
cos
x
=
(
sin
x
)
*
(
cot
x
)
;
:: thesis:
verum