theorem Them5: :: LAGRA4SQ:14

for p being Prime ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)