:: deftheorem defines are_coprime ARYTM_3:def 2 :
for a, b being Ordinal holds
( a,b are_coprime iff for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds
c = 1 );