let
a
,
b
be
Real
;
:: thesis:
(
a
>
0
implies
a
#R
b
>
0
)
assume
A1
:
a
>
0
;
:: thesis:
a
#R
b
>
0
then
a
#R
b
<>
0
by
Lm9
;
hence
a
#R
b
>
0
by
A1
,
Lm8
;
:: thesis:
verum