theorem :: REALALG3:44

for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for a being Element of F
for b, c being Element of E st b ^2 = a & c ^2 = - a & not P extends_to FAdj (F,{b}) holds
P extends_to FAdj (F,{c})