let F be ordered polynomial_disjoint Field; :: thesis: for a being non square Element of F st a in QS F holds
FAdj (F,{(sqrt a)}) is formally_real
let a be non square Element of F; :: thesis: ( a in QS F implies FAdj (F,{(sqrt a)}) is formally_real )
assume A: a in QS F ; :: thesis: FAdj (F,{(sqrt a)}) is formally_real
(sqrt a) ^2 = a by FIELD_9:53;
hence FAdj (F,{(sqrt a)}) is formally_real by A, FF1; :: thesis: verum