let F be Field; :: thesis: ( Char F <> 2 implies ( F is formally_real iff QS F is prepositive_cone ) )
assume AS: Char F <> 2 ; :: thesis: ( F is formally_real iff QS F is prepositive_cone )

hereby :: thesis: ( QS F is prepositive_cone implies F is formally_real )

assume F is formally_real ; :: thesis: QS F is prepositive_cone
then QS F is negative-disjoint by lemma1;
hence QS F is prepositive_cone ; :: thesis: verum

end;

assume QS F is prepositive_cone ; :: thesis: F is formally_real
then F is preordered ;
hence F is formally_real by AS, lemma3, lemma2; :: thesis: verum