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