take
(
n
,
n
)
-->
(
0.
K
)
;
:: thesis:
(
n
,
n
)
-->
(
0.
K
)
is
central_symmetric
thus
(
n
,
n
)
-->
(
0.
K
)
is
central_symmetric
;
:: thesis:
verum