theorem :: REALALG2:39

for F being formally_real Field
for a being Element of F holds
( ( for O being Ordering of F holds a in O ) iff a in QS F )