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