set A = the AlgebraicClosure of F;
take the AlgebraicClosure of F ; :: thesis: ( the AlgebraicClosure of F is F -algebraic & the AlgebraicClosure of F is F -normal )
thus ( the AlgebraicClosure of F is F -algebraic & the AlgebraicClosure of F is F -normal ) ; :: thesis: verum