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
a
#R
b
>
a
#R
0
by
A1
,
A2
,
Th83
;
hence
a
#R
b
>
1
by
A1
,
Th71
;
:: thesis:
verum