:: deftheorem Def10 defines / ARYTM_3:def 10 :
for i, j being natural Ordinal holds
( ( j = {} implies i / j = {} ) & ( RED (j,i) = 1 implies i / j = RED (i,j) ) & ( not j = {} & not RED (j,i) = 1 implies i / j = [(RED (i,j)),(RED (j,i))] ) );