:: deftheorem Def1 defines Pell's_solution PELLS_EQ:def 1 :
for D being Nat
for b₂ being Element of [:INT,INT:] holds
( b₂ is Pell's_solution of D iff ((b₂ `1) ^2) - (D * ((b<sub>2</sub> `2) ^2)) = 1 );