for x being Element of RAT+ holds denominator x <> {}