theorem :: REALALG2:30

for F being preordered Field
for P being Preordering of F holds
( P is maximal iff P is Ordering of F ) ;