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