theorem Th26: :: HILB10_6:26

for a being non trivial Nat
for y, n, b, c, d, r, s, t, u, v, x being Nat st 1 <= n & [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [s,t] is Pell's_solution of (b ^2) -' 1 & v = (4 * r) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y holds
( not b is trivial & u ^2 > a & y = Py (a,n) )