let F be formally_real Field; :: thesis: for E being FieldExtension of F
for a being Element of F
for b being Element of E st b ^2 = a & a in QS F holds
FAdj (F,{b}) is formally_real
let E be FieldExtension of F; :: thesis: for a being Element of F
for b being Element of E st b ^2 = a & a in QS F holds
FAdj (F,{b}) is formally_real
let a be Element of F; :: thesis: for b being Element of E st b ^2 = a & a in QS F holds
FAdj (F,{b}) is formally_real
let b be Element of E; :: thesis: ( b ^2 = a & a in QS F implies FAdj (F,{b}) is formally_real )
assume A: ( b ^2 = a & a in QS F ) ; :: thesis: FAdj (F,{b}) is formally_real
then I: b ^2 in F ;
set P = the Ordering of F;
assume B: not FAdj (F,{b}) is formally_real ; :: thesis: contradiction

C: now :: thesis: not the Ordering of F extends_to FAdj (F,{b})

assume the Ordering of F extends_to FAdj (F,{b}) ; :: thesis: contradiction
then consider O being Subset of (FAdj (F,{b})) such that
D: ( the Ordering of F c= O & O is positive_cone ) ;
FAdj (F,{b}) is ordered by D;
hence contradiction by B; :: thesis: verum

end;

QS F c= the Ordering of F by REALALG1:24;
hence contradiction by A, C, I, oext1; :: thesis: verum