A1
:
s
<=
0
by
XXREAL_0:def 6
;
A2
:
r
<=
0
by
XXREAL_0:def 6
;
per
cases
(
r
=
0
or
r
<
0
)
by
A2
,
Lm4
;
suppose
r
=
0
;
:: thesis:
not
r
+
s
is
positive
hence
r
+
s
<=
0
by
XXREAL_0:def 6
;
:: according to
XXREAL_0:def 6
:: thesis:
verum
end;
suppose
r
<
0
;
:: thesis:
not
r
+
s
is
positive
hence
r
+
s
<=
0
by
A1
,
Lm15
;
:: according to
XXREAL_0:def 6
:: thesis:
verum
end;
end;