theorem oext2: :: REALALG3:41

for F being ordered polynomial_disjoint Field
for P being Ordering of F
for a being non square Element of F holds
( P extends_to FAdj (F,{(sqrt a)}) iff a in P )