let R be non degenerated Ring; :: thesis: ( R is preordered implies R is formally_real )
assume R is preordered ; :: thesis: R is formally_real
then reconsider R = R as preordered Ring ;
QS R c= the Preordering of R by REALALG1:24;
hence R is formally_real by REALALG1:26; :: thesis: verum