let
a
,
b
be
Real
;
:: thesis:
(
a
>
1 &
b
<
0
implies
a
#R
b
<
1 )
assume
that
A1
:
a
>
1
and
A2
:
b
<
0
;
:: thesis:
a
#R
b
<
1

b
>
0
by
A2
;
then
a
#R
(

b
)
>
1
by
A1
,
Th86
;
then
1
/
(
a
#R
b
)
>
1
by
A1
,
Th76
;
then
1
/
(
1
/
(
a
#R
b
)
)
<
1
by
XREAL_1:212
;
hence
a
#R
b
<
1 ;
:: thesis:
verum