let F be Field; :: thesis: for E being F -algebraic FieldExtension of F ex A being AlgebraicClosure of F st E is Subfield of A
let E be F -algebraic FieldExtension of F; :: thesis: ex A being AlgebraicClosure of F st E is Subfield of A
set K = the AlgebraicClosure of E;
reconsider K = the AlgebraicClosure of E as FieldExtension of F ;
reconsider K = K as E -extending FieldExtension of F ;
K is F -algebraic by FIELD_7:39;
then reconsider K = K as AlgebraicClosure of F by defAC;
take K ; :: thesis: E is Subfield of K
thus E is Subfield of K by FIELD_4:7; :: thesis: verum