theorem T1: :: REALALG2:28

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