theorem :: PELLS_EQ:17

for D being non square Nat holds { ab where ab is positive Pell's_solution of D : verum } is infinite