X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1;
then Z: ( MinPoly (a,F) <> 0_. F & MinPoly (a,F) = NormPolynomial (MinPoly (a,F)) ) by X, ALGNUM_1:def 9;
then not MinPoly (a,F) is zero by UPROOTS:def 5;
hence MinPoly (a,F) is monic by Z; :: thesis: MinPoly (a,F) is irreducible
thus MinPoly (a,F) is irreducible by lemminirred; :: thesis: verum