let F be Field; :: thesis: ( F is formally_real implies (QS F) /\ (- (QS F)) = {(0. F)} )
assume A: F is formally_real ; :: thesis: (QS F) /\ (- (QS F)) = {(0. F)}
B: SQ F c= QS F by REALALG1:18;
(QS F) * (QS F) c= QS F

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (QS F) * (QS F) or o in QS F )
assume o in (QS F) * (QS F) ; :: thesis: o in QS F
then ex s1, s2 being Element of F st
( o = s1 * s2 & s1 in QS F & s2 in QS F ) ;
hence o in QS F by REALALG1:def 5; :: thesis: verum

end;

hence (QS F) /\ (- (QS F)) = {(0. F)} by A, B, REALALG1:21; :: thesis: verum