:: deftheorem defines HWZSet DIOPHAN2:def 2 :
for r being irrational Real holds HWZSet r = { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;