let F be ordered polynomial_disjoint Field; :: thesis: 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 )
let P be Ordering of F; :: thesis: for a being non square Element of F holds
( P extends_to FAdj (F,{(sqrt a)}) iff a in P )
let a be non square Element of F; :: thesis: ( P extends_to FAdj (F,{(sqrt a)}) iff a in P )
set b = sqrt a;
H: (sqrt a) ^2 = a by FIELD_9:53;
then (sqrt a) ^2 in F ;
hence ( P extends_to FAdj (F,{(sqrt a)}) iff a in P ) by H, oext1; :: thesis: verum