for x being Element of RAT+ holds
( x in omega iff denominator x = 1 ) by Def9, Th36;