theorem Th12: :: PELLS_EQ:12

for D being Nat st not D is square holds
{ [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } is infinite