let F be Field; :: thesis: ( F is algebraic-closed iff for E being F -finite FieldExtension of F holds E == F )

A: now :: thesis: ( F is algebraic-closed implies for E being F -finite FieldExtension of F holds E == F )

assume F is algebraic-closed ; :: thesis: for E being F -finite FieldExtension of F holds E == F
then F is maximal_algebraic by eq;
hence for E being F -finite FieldExtension of F holds E == F ; :: thesis: verum

end;

now :: thesis: ( not F is algebraic-closed implies ex E being F -finite FieldExtension of F st not E == F )

assume not F is algebraic-closed ; :: thesis: not for E being F -finite FieldExtension of F holds E == F
then not F is maximal_algebraic by eq;
then consider E being F -algebraic FieldExtension of F such that
B: not E == F ;
F is Subfield of E by FIELD_4:7;
then C: the carrier of F c= the carrier of E by EC_PF_1:def 1;
F: not deg (E,F) = 1 by B, FIELD_7:8;

now :: thesis: not for a being Element of E holds a in F

assume G: for a being Element of E holds a in F ; :: thesis: contradiction

now :: thesis: for o being object st o in the carrier of E holds
o in the carrier of F

let o be object ; :: thesis: ( o in the carrier of E implies o in the carrier of F )
assume o in the carrier of E ; :: thesis: o in the carrier of F
then reconsider a = o as Element of E ;
a in F by G;
hence o in the carrier of F ; :: thesis: verum

end;

hence contradiction by F, FIELD_7:7, C, TARSKI:2; :: thesis: verum

end;

then consider a being Element of E such that
D: not a in F ;
set p = MinPoly (a,F);
a in {a} by TARSKI:def 1;
then {a} is not Subset of F by D;
then not FAdj (F,{a}) == F by FIELD_7:3;
hence not for E being F -finite FieldExtension of F holds E == F ; :: thesis: verum

end;

hence ( F is algebraic-closed iff for E being F -finite FieldExtension of F holds E == F ) by A; :: thesis: verum