theorem :: REALALG3:45

for F being ordered polynomial_disjoint Field
for P being Ordering of F
for a, b being non square Element of F holds
( not b = - a or P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )