A1: ( r <= 0 & s <= 0 ) by XXREAL_0:def 6;

per cases ( r = 0 or s = 0 or ( - (- r) < - (- 0 ) & s < 0 ) ) by A1, Lm4;

suppose ( r = 0 or s = 0 ) ; :: thesis: not r * s is negative

hence r * s >= 0 ; :: according to XXREAL_0:def 7 :: thesis: verum

end;

suppose A2: ( - (- r) < - (- 0 ) & s < 0 ) ; :: thesis: not r * s is negative

then 0 < - r by Lm23;
then A3: s * (- r) <= 0 * (- r) by A2, Lm18;
s * (- r) <> 0 * (- r) by A2;
then s * (- r) < 0 * (- r) by A3, Lm4;
then - (- (0 * r)) < - (- (s * r)) by Lm23;
hence r * s >= 0 ; :: according to XXREAL_0:def 7 :: thesis: verum

end;

end;