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;