let r be irrational Real; :: thesis: { q where q is Rational : |.(r - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2)) } is infinite
HWZSet1 r is infinite ;
hence { q where q is Rational : |.(r - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2)) } is infinite by Th7; :: thesis: verum