let F be formally_real Field; :: thesis: for a being Element of F holds
( ( for O being Ordering of F holds a in O ) iff a in QS F )
let a be Element of F; :: thesis: ( ( for O being Ordering of F holds a in O ) iff a in QS F )
reconsider Q = QS F as Preordering of F ;
hereby :: thesis: ( a in QS F implies for O being Ordering of F holds a in O )
assume for O being Ordering of F holds a in O ; :: thesis: a in QS F
then for O being Ordering of F st Q c= O holds
a in O ;
then a in /\ (Q,F) ;
hence a in QS F by s1; :: thesis: verum
end;
assume AS: a in QS F ; :: thesis: for O being Ordering of F holds a in O
let O be Ordering of F; :: thesis: a in O
QS F c= O by REALALG1:24;
hence a in O by AS; :: thesis: verum