theorem Th9: :: PELLS_EQ:9

for n, D being Nat st not D is square & n > 1 holds
ex x, y being Integer st
( y <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n )