theorem FF1: :: REALALG3:46

for F being formally_real Field
for E being FieldExtension of F
for a being Element of F
for b being Element of E st b ^2 = a & a in QS F holds
FAdj (F,{b}) is formally_real