let D be non square Nat; :: thesis: { ab where ab is positive Pell's_solution of D : verum } is infinite
set P = { ab where ab is positive Pell's_solution of D : verum } ;
assume A1: { ab where ab is positive Pell's_solution of D : verum } is finite ; :: thesis: contradiction
set ab = the positive Pell's_solution of D;
A2: ( the positive Pell's_solution of D = [( the positive Pell's_solution of D `1),( the positive Pell's_solution of D `2)] & the positive Pell's_solution of D in { ab where ab is positive Pell's_solution of D : verum } ) ;
proj2 { ab where ab is positive Pell's_solution of D : verum } c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 { ab where ab is positive Pell's_solution of D : verum } or y in NAT )
assume y in proj2 { ab where ab is positive Pell's_solution of D : verum } ; :: thesis: y in NAT
then consider x being object such that
A3: [x,y] in { ab where ab is positive Pell's_solution of D : verum } by XTUPLE_0:def 13;
consider ab being positive Pell's_solution of D such that
A4: [x,y] = ab by A3;
( y = ab `2 & ab `2 > 0 ) by A4;
hence y in NAT by INT_1:3; :: thesis: verum

end;

then reconsider P2 = proj2 { ab where ab is positive Pell's_solution of D : verum } as non empty finite Subset of NAT by A1, WAYBEL26:39, A2, XTUPLE_0:def 13;
set b = max P2;
max P2 in P2 by XXREAL_2:def 8;
then consider a being object such that
A5: [a,(max P2)] in { ab where ab is positive Pell's_solution of D : verum } by XTUPLE_0:def 13;
consider ab being positive Pell's_solution of D such that
A6: [a,(max P2)] = ab by A5;
A7: ( a = ab `1 & max P2 = ab `2 ) by A6;
then reconsider a = a, b = max P2 as Nat ;
set A = (2 * (a ^2)) - 1;
set B = (2 * a) * b;
(a ^2) - ((b ^2) * D) = 1 by Lm4, A6;
then a ^2 = 1 + ((b ^2) * D) ;
then 1 = ((((4 * (a ^2)) * (a ^2)) - (4 * (a ^2))) + 1) - (((4 * (a ^2)) * (b ^2)) * D)
.= (((2 * (a ^2)) - 1) ^2) - ((((2 * a) * b) ^2) * D) ;
then reconsider AB = [((2 * (a ^2)) - 1),((2 * a) * b)] as Pell's_solution of D by Lm4;
a ^2 >= 1 by A7, NAT_1:14;
then (a ^2) + (a ^2) >= 1 + 1 by XREAL_1:7;
then (2 * (a ^2)) - 1 >= (1 + 1) - 1 by XREAL_1:9;
then ( AB `1 > 0 & AB `2 > 0 ) by A7;
then AB is positive Pell's_solution of D by Def2;
then AB in { ab where ab is positive Pell's_solution of D : verum } ;
then A8: (2 * a) * b in P2 by XTUPLE_0:def 13;
a >= 1 by A7, NAT_1:14;
then a + a > 1 + 0 by XREAL_1:8;
then (2 * a) * b > 1 * b by A7, XREAL_1:68;
hence contradiction by A8, XXREAL_2:def 8; :: thesis: verum