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 >= 0 * s by Lm16;
hence r * s > 0 by A1, Lm4; :: thesis: verum