let F be Field; :: thesis: ex E being Field st E is AlgebraicClosure of F
set A = the AlgebraicClosure of F;
take the AlgebraicClosure of F ; :: thesis: the AlgebraicClosure of F is AlgebraicClosure of F
thus the AlgebraicClosure of F is AlgebraicClosure of F ; :: thesis: verum