let a, b be real number ; :: thesis: ( a > 1 & b > 0 implies a #R b > 1 )
assume A1: ( a > 1 & b > 0 ) ; :: thesis: a #R b > 1
then a #R b > a #R 0 by Th97;
hence a #R b > 1 by A1, Th85; :: thesis: verum