theorem Th60: :: NUMBER03:60
for k being Nat
for p being Prime st p = (4 * k) + 1 holds
ex a, b being positive Nat st
( a > b & p = (a ^2) + (b ^2) )