theorem lemma3: :: FIELD_8:28

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b₃ -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= Roots (U,p) )