:: deftheorem Def3 defines polynomial_disjoint FIELD_3:def 3 :
for R being Ring holds
( R is polynomial_disjoint iff ([#] R) /\ ([#] (Polynom-Ring R)) = {} );