take
(
n
,
n
)
-->
(
In
(1,
REAL
)
)
;
:: thesis:
( (
n
,
n
)
-->
(
In
(1,
REAL
)
)
is
Positive
& (
n
,
n
)
-->
(
In
(1,
REAL
)
)
is
Nonnegative
)
thus
( (
n
,
n
)
-->
(
In
(1,
REAL
)
)
is
Positive
& (
n
,
n
)
-->
(
In
(1,
REAL
)
)
is
Nonnegative
) ;
:: thesis:
verum