A1: ( r >= 0 & s >= 0 ) by XXREAL_0:def 7;

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 ( r > 0 & s > 0 ) ; :: thesis: not r * s is negative

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

end;

end;