take
(1,1)
>
(

(
In
(1,
REAL
)
)
)
;
:: thesis:
( (1,1)
>
(

(
In
(1,
REAL
)
)
)
is
Negative
& (1,1)
>
(

(
In
(1,
REAL
)
)
)
is
Nonpositive
)
thus
( (1,1)
>
(

(
In
(1,
REAL
)
)
)
is
Negative
& (1,1)
>
(

(
In
(1,
REAL
)
)
)
is
Nonpositive
) ;
:: thesis:
verum