A: {(sqrt a)} is Subset of (FAdj (F,{(sqrt a)})) by FIELD_6:35;
sqrt a in {(sqrt a)} by TARSKI:def 1;
hence sqrt a is FAdj (F,{(sqrt a)}) -membered by A, FIELD_7:def 5; :: thesis: not sqrt a is F -membered

now :: thesis: not sqrt a is F -membered

assume B: sqrt a is F -membered ; :: thesis: contradiction
then reconsider sqrta = sqrt a as Element of F by FIELD_7:def 5;
C: deg (rpoly (1,sqrta)) = 1 by HURWITZ:27;
D: rpoly (1,sqrta) = rpoly (1,(sqrt a)) by FIELD_4:21;
MinPoly ((sqrt a),F) = rpoly (1,(sqrt a)) by B, FIELD_7:def 5, FIELD_6:54;
then deg ((FAdj (F,{(sqrt a)})),F) = deg (rpoly (1,sqrta)) by D, FIELD_6:67;
hence contradiction by C, dega; :: thesis: verum

end;

hence not sqrt a is F -membered ; :: thesis: verum