let K, L be Field; :: thesis: for w being Element of L st K is Subring of L & w is_integral_over K holds
Ann_Poly (w,K) is prime
let w be Element of L; :: thesis: ( K is Subring of L & w is_integral_over K implies Ann_Poly (w,K) is prime )
assume ( K is Subring of L & w is_integral_over K ) ; :: thesis: Ann_Poly (w,K) is prime
then ( Ann_Poly (w,K) is proper & Ann_Poly (w,K) is quasi-prime ) by Th38, Th33;
hence Ann_Poly (w,K) is prime ; :: thesis: verum