theorem :: REALALG2:40

for r being Element of F_Rat st 0 <= r holds
r is sum_of_squares