:: deftheorem defines RAT+ ARYTM_3:def 7 :
RAT+ = ( { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega;