take QS R ; :: thesis: QS R is with_sums_of_squares
thus QS R is with_sums_of_squares ; :: thesis: verum