:: deftheorem defines *' ARYTM_2:def 7 :
for A, B being Element of DEDEKIND_CUTS holds A *' B = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;