theorem :: REALALG2:38

for F being formally_real Field holds QS F is Preordering of F ;