A1
: (
r
>=
0
&
s
>=
0
)
by
XXREAL_0:def 7
;
per
cases
(
r
=
0
or
s
=
0
or (
r
>
0
&
s
>
0
) )
by
A1
,
Lm4
;
suppose
(
r
=
0
or
s
=
0
) ;
:: thesis:
not
r
*
s
is
negative
hence
r
*
s
>=
0
;
:: according to
XXREAL_0:def 7
:: thesis:
verum
end;
suppose
(
r
>
0
&
s
>
0
) ;
:: thesis:
not
r
*
s
is
negative
hence
r
*
s
>=
0
by
Lm17
;
:: according to
XXREAL_0:def 7
:: thesis:
verum
end;
end;