theorem Lagrange4Squares: :: LAGRA4SQ:18

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