theorem :: REALALG3:48

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