theorem T0: :: REALALG2:34

for F being Field st Char F <> 2 holds
( F is formally_real iff QS F is prepositive_cone )