let r, s be Real; :: thesis: ( r <= 0 & s >= 0 implies r * s <= 0 )
assume A1: ( r <= 0 & s >= 0 ) ; :: thesis: r * s <= 0

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

suppose ( r = 0 or s = 0 ) ; :: thesis: r * s <= 0

hence r * s <= 0 ; :: thesis: verum

end;

suppose ( r < 0 & s > 0 ) ; :: thesis: r * s <= 0

hence r * s <= 0 by Lm18; :: thesis: verum

end;

end;