:: deftheorem defines formally_real REALALG2:def 3 :
for R being Ring holds
( R is formally_real iff not - (1. R) in QS R );