theorem :: ARYTM_3:78

for r, s being Element of RAT+ holds
( not r *' s = {} or r = {} or s = {} )