:: deftheorem Def3 defines min_Pell's_solution_of PELLS_EQ:def 3 :
for D being non square Nat
for b₂ being positive Pell's_solution of D holds
( b₂ = min_Pell's_solution_of D iff for p being positive Pell's_solution of D holds
( b₂ `1 <= p `1 & b₂ `2 <= p `2 ) );