set RX = Polynom-Ring R;

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

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

now :: thesis: Polynom-Ring R is polynomial_disjoint

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