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