theorem Th45: :: DIOPHAN2:33

for a1, b1 being Real
for n1, d1 being Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) holds
ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )