theorem oext1: :: REALALG3:40

for F being ordered Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
for P being Ordering of F holds
( P extends_to FAdj (F,{a}) iff a ^2 in P )