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;