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