let x, y be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not x in QS R or not y in QS R or x + y in QS R )
assume AS: ( x in QS R & y in QS R ) ; :: thesis: x + y in QS R
then consider a being Element of R such that
A: ( x = a & a is sum_of_squares ) ;
consider b being Element of R such that
B: ( y = b & b is sum_of_squares ) by AS;
thus x + y in QS R by A, B; :: thesis: verum