let
r
,
s
be
Real
;
:: thesis:
(
r
<=
0
&
s
<
0
implies
r
+
s
<
0
)
assume
r
<=
0
;
:: thesis:
( not
s
<
0
or
r
+
s
<
0
)
then
r
+
s
<=
0
+
s
by
Lm5
;
hence
( not
s
<
0
or
r
+
s
<
0
)
by
Lm6
;
:: thesis:
verum