let n be square Nat; for p being positive Element of [:INT,INT:] st n > 0 holds
not p is Pell's_solution of n
consider m being Nat such that
A1:
n = m ^2
by PYTHTRIP:def 3;
let p be positive Element of [:INT,INT:]; ( n > 0 implies not p is Pell's_solution of n )
set p1 = p `1 ;
set p2 = p `2 ;
assume A2:
( n > 0 & p is Pell's_solution of n )
; contradiction
then
((p `1) ^2) - (n * ((p `2) ^2)) = 1
by Def1;
then A3:
((p `1) - (m * (p `2))) * ((p `1) + (m * (p `2))) = 1
by A1;