:: deftheorem Sum4Sq defines a_sum_of_four_squares LAGRA4SQ:def 1 :
for n being natural number holds
( n is a_sum_of_four_squares iff ex n1, n2, n3, n4 being Nat st n = (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) );