set RX = Polynom-Ring R;
set x = the Element of ([#] (Polynom-Ring R)) /\ ([#] (Polynom-Ring (Polynom-Ring R)));

now :: thesis: Polynom-Ring R is polynomial_disjoint

assume not Polynom-Ring R is polynomial_disjoint ; :: thesis: contradiction
then A1: ( the Element of ([#] (Polynom-Ring R)) /\ ([#] (Polynom-Ring (Polynom-Ring R))) in [#] (Polynom-Ring R) & the Element of ([#] (Polynom-Ring R)) /\ ([#] (Polynom-Ring (Polynom-Ring R))) in [#] (Polynom-Ring (Polynom-Ring R)) ) by XBOOLE_0:def 4;
then reconsider p1 = the Element of ([#] (Polynom-Ring R)) /\ ([#] (Polynom-Ring (Polynom-Ring R))) as Polynomial of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider p2 = the Element of ([#] (Polynom-Ring R)) /\ ([#] (Polynom-Ring (Polynom-Ring R))) as Polynomial of R by A1, POLYNOM3:def 10;
p2 . 0 in [#] R ;
then p1 . 0 in ([#] R) /\ ([#] (Polynom-Ring R)) by XBOOLE_0:def 4;
hence contradiction by Def3; :: thesis: verum

end;

hence Polynom-Ring R is polynomial_disjoint ; :: thesis: verum