let F be ordered polynomial_disjoint Field; :: thesis: for P being Ordering of F
for a, b being non square Element of F holds
( not b = - a or P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )
let P be Ordering of F; :: thesis: for a, b being non square Element of F holds
( not b = - a or P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )
let a, b be non square Element of F; :: thesis: ( not b = - a or P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )
H: P \/ (- P) = the carrier of F by REALALG1:def 15;
assume A: b = - a ; :: thesis: ( P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )

per cases ( a in P or not a in P ) ;

suppose a in P ; :: thesis: ( P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )

hence ( P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) ) by oext2; :: thesis: verum

end;

suppose not a in P ; :: thesis: ( P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) )

then a in - P by H, XBOOLE_0:def 3;
then - a in - (- P) ;
hence ( P extends_to FAdj (F,{(sqrt a)}) or P extends_to FAdj (F,{(sqrt b)}) ) by A, oext2; :: thesis: verum

end;

end;