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