theorem Th19: :: PELLS_EQ:19

for D being Nat
for p1, p2 being Pell's_solution of D st 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square holds
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )