let F be Field; :: thesis: ( F is maximal_algebraic iff F is algebraic-closed )

A: now :: thesis: ( F is maximal_algebraic implies F is algebraic-closed )

assume B: F is maximal_algebraic ; :: thesis: F is algebraic-closed

now :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds 1 = deg p

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: 1 = deg p
consider E being F -finite FieldExtension of F such that
C: ( deg (E,F) = deg p & p is_with_roots_in E ) by mi2;
thus 1 = deg p by C, B, FIELD_7:8; :: thesis: verum

end;

hence F is algebraic-closed by al1; :: thesis: verum

end;

now :: thesis: ( not F is maximal_algebraic implies not F is algebraic-closed )

assume not F is maximal_algebraic ; :: thesis: not F is algebraic-closed
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);
E: deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F)) by FIELD_6:67;
a in {a} by TARSKI:def 1;
then {a} is not Subset of F by D;
then not deg ((FAdj (F,{a})),F) = 1 by FIELD_7:8, FIELD_7:3;
hence not F is algebraic-closed by E, al1; :: thesis: verum

end;

hence ( F is maximal_algebraic iff F is algebraic-closed ) by A; :: thesis: verum