let F be Field; :: thesis: ( Char F <> 2 implies ( F is formally_real iff ex P being Subset of F st P is prepositive_cone ) )
assume AS: Char F <> 2 ; :: thesis: ( F is formally_real iff ex P being Subset of F st P is prepositive_cone )

hereby :: thesis: ( ex P being Subset of F st P is prepositive_cone implies F is formally_real )

assume F is formally_real ; :: thesis: ex P being Subset of F st P is prepositive_cone
then QS F is negative-disjoint by lemma1;
hence ex P being Subset of F st P is prepositive_cone ; :: thesis: verum

end;

assume ex P being Subset of F st P is prepositive_cone ; :: thesis: F is formally_real
then F is preordered ;
hence F is formally_real by AS, lemma3, lemma2; :: thesis: verum