theorem Th14: :: PELLS_EQ:14

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