let R be preordered Ring; :: thesis: for P being Preordering of R holds QS R c= P
let P be Preordering of R; :: thesis: QS R c= P
P is with_sums_of_squares ;
hence QS R c= P ; :: thesis: verum