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

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

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

end;

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

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

end;

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