( r > 0 & s >= 0 ) by XXREAL_0:def 6;
hence r + s > 0 by Lm14; :: according to XXREAL_0:def 6 :: thesis: verum