theorem :: REALALG3:49

for F being ordered polynomial_disjoint Field
for a being non square Element of F st not FAdj (F,{(sqrt a)}) is formally_real holds
- a in QS F