let S be Subset of R; :: thesis: ( S is with_sums_of_squares implies S is with_squares )
assume AS: S is with_sums_of_squares ; :: thesis: S is with_squares
SQ R c= S

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ R or o in S )
assume o in SQ R ; :: thesis: o in S
then consider a being Element of R such that
A: ( o = a & a is square ) ;
a in QS R by A;
hence o in S by A, AS; :: thesis: verum

end;

hence S is with_squares ; :: thesis: verum