( r < 0 & s <= 0 ) by XXREAL_0:def 7;
hence r + s < 0 by Lm15; :: according to XXREAL_0:def 7 :: thesis: verum