let R be non degenerated preordered Ring; :: thesis: QS R <> the carrier of R
set P = the Preordering of R;
( QS R c= the Preordering of R & not - (1. R) in the Preordering of R ) by REALALG1:26, REALALG1:24;
hence QS R <> the carrier of R ; :: thesis: verum