let R be Ring; :: thesis: ( R is strong_polynomial_disjoint implies R is polynomial_disjoint )
assume A: R is strong_polynomial_disjoint ; :: thesis: R is polynomial_disjoint
set o = the Element of the carrier of R /\ the carrier of (Polynom-Ring R);

now :: thesis: R is polynomial_disjoint

assume not R is polynomial_disjoint ; :: thesis: contradiction
then ([#] R) /\ ([#] (Polynom-Ring R)) <> {} by FIELD_3:def 3;
then ( the Element of the carrier of R /\ the carrier of (Polynom-Ring R) in the carrier of R & the Element of the carrier of R /\ the carrier of (Polynom-Ring R) in the carrier of (Polynom-Ring R) ) by XBOOLE_0:def 4;
hence contradiction by A; :: thesis: verum

end;

hence R is polynomial_disjoint ; :: thesis: verum