for a, b being natural Ordinal st b <> {} holds
( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) )