theorem :: FIELD_5:26

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