theorem :: REALALG2:37

for F being Field st Char F <> 2 holds
( F is formally_real iff QS F <> the carrier of F ) by lemma3;