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

HWZSet1 r is infinite ;

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