defpred S₁[ Nat] means ex p being positive Pell's_solution of D st p `1 = $1;
set p = the positive Pell's_solution of D;
reconsider p1 = the positive Pell's_solution of D `1 as Element of NAT by INT_1:3;
S₁[p1] ;
then A1: ex n being Nat st S₁[n] ;
consider m being Nat such that
A2: ( S₁[m] & ( for n being Nat st S₁[n] holds
m <= n ) ) from NAT_1:sch 5(A1);
consider p being positive Pell's_solution of D such that
A3: p `1 = m by A2;
take p ; :: thesis: for p being positive Pell's_solution of D holds
( p `1 <= p `1 & p `2 <= p `2 )
let q be positive Pell's_solution of D; :: thesis: ( p `1 <= q `1 & p `2 <= q `2 )
set pp = (p `1) + ((p `2) * (sqrt D));
set qq = (q `1) + ((q `2) * (sqrt D));
A4: ( (p `1) + ((p `2) * (sqrt D)) > 1 & (q `1) + ((q `2) * (sqrt D)) > 1 & q `1 in NAT ) by Th18, INT_1:3;
( (p `1) + ((p `2) * (sqrt D)) > (q `1) + ((q `2) * (sqrt D)) or (p `1) + ((p `2) * (sqrt D)) = (q `1) + ((q `2) * (sqrt D)) or (p `1) + ((p `2) * (sqrt D)) < (q `1) + ((q `2) * (sqrt D)) ) by XXREAL_0:1;
hence ( p `1 <= q `1 & p `2 <= q `2 ) by A2, A3, A4, Th19, Th3; :: thesis: verum