let F be ordered Field; :: thesis: 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})
let P be Ordering of F; :: thesis: 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})
let E be FieldExtension of F; :: thesis: 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})
let a be Element of F; :: thesis: 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})
let b, c be Element of E; :: thesis: ( b ^2 = a & c ^2 = - a & not P extends_to FAdj (F,{b}) implies P extends_to FAdj (F,{c}) )
assume AS: ( b ^2 = a & c ^2 = - a ) ; :: thesis: ( P extends_to FAdj (F,{b}) or P extends_to FAdj (F,{c}) )
H: P \/ (- P) = the carrier of F by REALALG1:def 15;
I: ( b ^2 in F & c ^2 in F ) by AS;
assume not P extends_to FAdj (F,{b}) ; :: thesis: P extends_to FAdj (F,{c})
then not b ^2 in P by I, oext1;
then a in - P by AS, H, XBOOLE_0:def 3;
then c ^2 in - (- P) by AS;
hence P extends_to FAdj (F,{c}) by I, oext1; :: thesis: verum