theorem :: DIOPHAN2:14

for r being irrational Real holds { q where q is Rational : |.(r - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2)) } is infinite