let a, b be Real; :: thesis: ( a > 0 implies a #R b > 0 )
assume A1: a > 0 ; :: thesis: a #R b > 0
then a #R b <> 0 by Lm9;
hence a #R b > 0 by A1, Lm8; :: thesis: verum