for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being polynomial_disjoint Field st E = embField (emb p) holds
F is polynomial_disjoint