for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= Roots (S,p)