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

set M = ([#] R) /\ ([#] (Polynom-Ring R));

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

now :: thesis: R is polynomial_disjoint

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