A1: ( r >= 0 & s >= 0 ) by XXREAL_0:def 7;

per cases ( r = 0 or r > 0 ) by A1, 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, Lm16; :: according to XXREAL_0:def 7 :: thesis: verum

end;

end;