theorem :: NUMBER15:88

for a being Real
for k, x, y being positive Nat st a > 0 & (x |^ (2 * k)) - (y |^ (2 * k)) = a holds
( x < k -Root a & y < k -Root a )