let
r
,
s
be
Real
;
:: thesis:
(
r
<=
0
&
s
>=
0
implies
r
*
s
<=
0
)
assume
A1
: (
r
<=
0
&
s
>=
0
) ;
:: thesis:
r
*
s
<=
0
per
cases
(
r
=
0
or
s
=
0
or (
r
<
0
&
s
>
0
) )
by
A1
,
Lm4
;
suppose
(
r
=
0
or
s
=
0
) ;
:: thesis:
r
*
s
<=
0
hence
r
*
s
<=
0
;
:: thesis:
verum
end;
suppose
(
r
<
0
&
s
>
0
) ;
:: thesis:
r
*
s
<=
0
hence
r
*
s
<=
0
by
Lm18
;
:: thesis:
verum
end;
end;