theorem Th3: :: PELLS_EQ:3

for D being non square Nat
for a, b, c, d being Integer st a + (b * (sqrt D)) = c + (d * (sqrt D)) holds
( a = c & b = d )