theorem FF2: :: REALALG3:47

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 & not FAdj (F,{b}) is formally_real holds
- a in QS F