theorem :: ARYTM_3:22

for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds
RED (a,b), RED (b,a) are_coprime by Th19;