let F be Field; :: thesis: ( F is ordered implies F is formally_real )
assume AS: F is ordered ; :: thesis: F is formally_real
then Char F = 0 by REALALG1:28;
hence F is formally_real by AS, T2; :: thesis: verum