for r being irrational Real
for r1 being non negative Real ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r )