for K, L being Field
for z being Element of L st z is_integral_over K holds
Ann_Poly (z,K) <> {(0. (Polynom-Ring K))}