:: deftheorem defines is_with_roots_in FIELD_4:def 3 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R) holds
( p is_with_roots_in S iff ex a being Element of S st a is_a_root_of p,S );