theorem T2: :: REALALG2:36

for F being Field st Char F <> 2 holds
( F is formally_real iff ex P being Subset of F st P is positive_cone )