let D be Nat; :: thesis: ( not D is square implies ex p being Pell's_solution of D st p is positive )
assume not D is square ; :: thesis: ex p being Pell's_solution of D st p is positive
then consider x, y being Nat such that
A1: ( (x ^2) - (D * (y ^2)) = 1 & y <> 0 ) by Th14;
( x in INT & y in INT ) by INT_1:def 2;
then reconsider ab = [x,y] as Element of [:INT,INT:] by ZFMISC_1:87;
( x = ab `1 & y = ab `2 ) ;
then reconsider ab = ab as Pell's_solution of D by A1, Def1;
take ab ; :: thesis: ab is positive
thus ab is positive by A1; :: thesis: verum