let F be Field; :: thesis: ex E being FieldExtension of F st E is algebraic-closed
set f = the ClosureSequence of F;
take E = SeqField the ClosureSequence of F; :: thesis: E is algebraic-closed
thus E is algebraic-closed ; :: thesis: verum