let a, b be Real; :: thesis: ( a > 0 implies a #R b <> 0 )
assume A1: a > 0 ; :: thesis: a #R b <> 0
assume a #R b = 0 ; :: thesis: contradiction
then 0 = (a #R b) * (a #R (- b))
.= a #R (b + (- b)) by A1, Th75
.= 1 by A1, Th71 ;
hence contradiction ; :: thesis: verum