let F be Field; :: thesis: ( F is formally_real implies F is ordered )
assume F is formally_real ; :: thesis: F is ordered
then QS F is negative-disjoint by lemma1;
then F is preordered ;
hence F is ordered ; :: thesis: verum