let r, s be Real; :: thesis: ( r > 0 & s < 0 implies r * s < 0 )
assume A1: ( r > 0 & s < 0 ) ; :: thesis: r * s < 0
then r * s <= r * 0 by Lm16;
hence r * s < 0 by A1, Lm4; :: thesis: verum