for n1, n2 being Nat
for a being non trivial Nat st [n1,n2] is Pell's_solution of (a ^2) -' 1 holds
ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )