for m1 being Nat
for i1 being Integer
for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds
( i1 = numerator q & m1 = denominator q )