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);

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

hence
R is polynomial_disjoint
; :: thesis: verumassume
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;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