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;