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