let F be Field; :: thesis: for E being FieldExtension of F
for A being AlgebraicClosure of F st A is E -extending holds
A is AlgebraicClosure of E
let E be FieldExtension of F; :: thesis: for A being AlgebraicClosure of F st A is E -extending holds
A is AlgebraicClosure of E
let A be AlgebraicClosure of F; :: thesis: ( A is E -extending implies A is AlgebraicClosure of E )
assume A is E -extending ; :: thesis: A is AlgebraicClosure of E
then reconsider B = A as FieldExtension of E ;
B is E -algebraic by FIELD_7:40;
hence A is AlgebraicClosure of E by defAC; :: thesis: verum