let
r
,
s
be
Real
;
:: thesis:
(
r
>
0
&
s
<
0
implies
r
*
s
<
0
)
assume
A1
: (
r
>
0
&
s
<
0
) ;
:: thesis:
r
*
s
<
0
then
r
*
s
<=
r
*
0
by
Lm16
;
hence
r
*
s
<
0
by
A1
,
Lm4
;
:: thesis:
verum