let R be flat Ring; :: thesis: R is polynomial_disjoint
set M = ([#] R) /\ ([#] (Polynom-Ring R));
set x = the Element of ([#] R) /\ ([#] (Polynom-Ring R));

now :: thesis: R is polynomial_disjoint

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

end;

hence R is polynomial_disjoint ; :: thesis: verum