( r <= 0 & s >= 0 ) by XXREAL_0:def 6;
hence r * s <= 0 by Lm20; :: according to XXREAL_0:def 6 :: thesis: verum