for r being irrational Real
for a1, a2, b1, b2 being Element of REAL
for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds
ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )