:: deftheorem dspd defines strong_polynomial_disjoint FIELD_5:def 4 :
for R being Ring holds
( R is strong_polynomial_disjoint iff for a being Element of R
for S being Ring
for p being Element of the carrier of (Polynom-Ring S) holds a <> p );