let F be preordered Field; :: thesis: F is ordered
ex Q being Preordering of F st
( the Preordering of F c= Q & Q is maximal ) by T3;
hence F is ordered ; :: thesis: verum