theorem Th11: :: PELLS_EQ:11

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